ody>
Theory StandardBorel
section â¹Standard Borel Spacesâº
theory StandardBorel
imports "HOL-Probability.Probability"
begin
text â¹A standard Borel space is the Borel space associated with a Polish space.
Here, we define standard Borel spaces in another, but equivallent, way.
See @{cite "Heunen_2017"} Proposition 5. âº
abbreviation "real_borel â¡ borel :: real measure"
abbreviation "nat_borel â¡ borel :: nat measure"
abbreviation "ennreal_borel â¡ borel :: ennreal measure"
abbreviation "bool_borel â¡ borel :: bool measure"
subsection â¹ Definition âº
locale standard_borel =
fixes M :: "'a measure"
assumes exist_fg: "âf â M ââ©M real_borel. âg â real_borel ââ©M M.
âx â space M. (g â f) x = x"
begin
abbreviation "fg â¡ (SOME k. (fst k) â M ââ©M real_borel â§
(snd k) â real_borel ââ©M M â§
(âx â space M. ((snd k) â (fst k)) x = x))"
definition "f â¡ (fst fg)"
definition "g â¡ (snd fg)"
lemma
shows f_meas[simp,measurable] : "f â M ââ©M real_borel"
and g_meas[simp,measurable] : "g â real_borel ââ©M M"
and gf_comp_id[simp]: "âx. x â space M â¹ (g â f) x = x"
"âx. x â space M â¹ g (f x) = x"
proof -
obtain f' g' where h:
"f' â M ââ©M real_borel" "g' â real_borel ââ©M M" "âx â space M. (g' â f') x = x"
using exist_fg by blast
have "f â borel_measurable M â§ g â real_borel ââ©M M â§ (âxâspace M. (g â f) x = x)"
unfolding f_def g_def
by(rule someI2[where a="(f',g')"]) (use h in auto)
thus "f â borel_measurable M" "g â real_borel ââ©M M"
"âx. x â space M â¹ (g â f) x = x" "âx. x â space M â¹ g (f x) = x"
by auto
qed
lemma standard_borel_sets[simp]:
assumes "sets M = sets Y"
shows "standard_borel Y"
unfolding standard_borel_def
using measurable_cong_sets[OF assms refl,of real_borel] measurable_cong_sets[OF refl assms,of real_borel] sets_eq_imp_space_eq[OF assms] exist_fg
by simp
lemma f_inj:
"inj_on f (space M)"
by standard (use gf_comp_id(2) in fastforce)
lemma singleton_sets:
assumes "x â space M"
shows "{x} â sets M"
proof -
let ?y = "f x"
let ?U = "f -` {?y}"
have "?U â© space M â sets M"
using borel_measurable_vimage f_meas by blast
moreover have "?U â© space M = {x}"
using assms f_inj by(auto simp:inj_on_def)
ultimately show ?thesis
by simp
qed
lemma countable_space_discrete:
assumes "countable (space M)"
shows "sets M = sets (count_space (space M))"
proof
show "sets (count_space (space M)) â sets M"
proof auto
fix U
assume 1:"U â space M"
then have 2:"countable U"
using assms countable_subset by auto
have 3:"U = (âxâU. {x})" by auto
moreover have "... â sets M"
by(rule sets.countable_UN''[of U "λx. {x}"]) (use 1 2 singleton_sets in auto)
ultimately show "U â sets M"
by simp
qed
qed (simp add: sets.sets_into_space subsetI)
end
lemma standard_borelI:
assumes "f â Y ââ©M real_borel"
"g â real_borel ââ©M Y"
and "ây. y â space Y â¹ (g â f) y = y"
shows "standard_borel Y"
unfolding standard_borel_def
by (intro bexI[OF _ assms(1)] bexI[OF _ assms(2)]) (auto dest: assms(3))
locale standard_borel_space_UNIV = standard_borel +
assumes space_UNIV:"space M = UNIV"
begin
lemma gf_comp_id'[simp]:
"g â f = id" "g (f x) = x"
using space_UNIV gf_comp_id
by(simp_all add: id_def comp_def)
lemma f_inj':
"inj f"
using f_inj by(simp add: space_UNIV)
lemma g_surj':
"surj g"
using gf_comp_id'(2) surjI by blast
end
lemma standard_borel_space_UNIVI:
assumes "f â Y ââ©M real_borel"
"g â real_borel ââ©M Y"
"(g â f) = id"
and "space Y = UNIV"
shows "standard_borel_space_UNIV Y"
using assms
by(auto intro!: standard_borelI simp: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def)
lemma standard_borel_space_UNIVI':
assumes "standard_borel Y"
and "space Y = UNIV"
shows "standard_borel_space_UNIV Y"
using assms by(simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def)
subsection â¹ $\mathbb{R}$, $\mathbb{N}$, Boolean, $[0,\infty]$ âº
text â¹ $\mathbb{R}$ is a standard Borel space. âº
interpretation real : standard_borel_space_UNIV "real_borel"
by(auto intro!: standard_borel_space_UNIVI)
textâ¹ A non-empty Borel subspace of $\mathbb{R}$ is also a standard Borel space. âº
lemma real_standard_borel_subset:
assumes "U â sets real_borel"
and "U â {}"
shows "standard_borel (restrict_space real_borel U)"
proof -
have std1: "id â (restrict_space real_borel U) ââ©M real_borel"
by (simp add: measurable_restrict_space1)
obtain x where hx : "x â U"
using assms(2) by auto
define g :: "real â real"
where "g â¡ (λr. if r â U then r else x)"
have "g â real_borel ââ©M real_borel"
unfolding g_def by(rule borel_measurable_continuous_on_if) (simp_all add: assms(1))
hence std2: "g â real_borel ââ©M (restrict_space real_borel U)"
by(auto intro!: measurable_restrict_space2 simp: g_def hx)
have std3: "âyâ space (restrict_space real_borel U). (g â id) y = y"
by(simp add: g_def space_restrict_space)
show ?thesis
using std1 std2 std3 standard_borel_def by blast
qed
text â¹ A non-empty measurable subset of a standard Borel space is also a standard Borel space.âº
lemma(in standard_borel) standard_borel_subset:
assumes "U â sets M"
"U â {}"
shows "standard_borel (restrict_space M U)"
proof -
let ?ginvU = "g -` U"
have hgu1:"?ginvU â sets real_borel"
using assms(1) g_meas measurable_sets_borel by blast
have hgu2:"f ` U â ?ginvU"
using gf_comp_id sets.sets_into_space[OF assms(1)] by fastforce
hence hgu3:"?ginvU â {}"
using assms(2) by blast
interpret r_borel_set: standard_borel "restrict_space real_borel ?ginvU"
by(rule real_standard_borel_subset[OF hgu1 hgu3])
have std1: "r_borel_set.f â f â (restrict_space M U) ââ©M real_borel"
using sets.sets_into_space[OF assms(1)]
by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3)
have std2: "g â r_borel_set.g â real_borel ââ©M (restrict_space M U)"
by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3[OF g_meas])
have std3: "âxâ space (restrict_space M U). ((g â r_borel_set.g) â (r_borel_set.f â f)) x = x"
by (simp add: space_restrict_space)
show ?thesis
using std1 std2 std3 standard_borel_def by blast
qed
text â¹ $\mathbb{N}$ is a standard Borel space. âº
interpretation nat : standard_borel_space_UNIV nat_borel
proof -
define n_to_r :: "nat â real"
where "n_to_r ⡠(λn. of_real n)"
define r_to_n :: "real â nat"
where "r_to_n â¡ (λr. nat ârâ)"
have n_to_r_measurable: "n_to_r â nat_borel ââ©M real_borel"
using borel_measurable_count_space measurable_cong_sets sets_borel_eq_count_space
by blast
have r_to_n_measurable: "r_to_n â real_borel ââ©M nat_borel"
by(simp add: r_to_n_def)
have n_to_r_to_n_id: "r_to_n â n_to_r = id"
by(simp add: n_to_r_def r_to_n_def comp_def id_def)
show "standard_borel_space_UNIV nat_borel"
using standard_borel_space_UNIVI[OF n_to_r_measurable r_to_n_measurable n_to_r_to_n_id]
by simp
qed
text â¹ For a countable space $X$, $X$ is a standard Borel space iff $X$ is a discrete space. âº
lemma countable_standard_iff:
assumes "space X â {}"
and "countable (space X)"
shows "standard_borel X â· sets X = sets (count_space (space X))"
proof
show "standard_borel X â¹ sets X = sets (count_space (space X))"
using standard_borel.countable_space_discrete assms by simp
next
assume h[measurable_cong]: "sets X = sets (count_space (space X))"
show "standard_borel X"
proof(rule standard_borelI[where f="nat.f â to_nat_on (space X)" and g="from_nat_into (space X) â nat.g"])
show "nat.f â to_nat_on (space X) â borel_measurable X"
by simp
next
have [simp]: "from_nat_into (space X) â UNIV â (space X)"
using from_nat_into[OF assms(1)] by simp
hence [measurable]: "from_nat_into (space X) â nat_borel ââ©M X"
using measurable_count_space_eq1[of _ _ X] measurable_cong_sets[OF sets_borel_eq_count_space]
by blast
show "from_nat_into (space X) â nat.g â real_borel ââ©M X"
by simp
next
fix x
assume "x â space X"
then show "(from_nat_into (space X) â nat.g â (nat.f â to_nat_on (space X))) x = x"
using from_nat_into_to_nat_on[OF assms(2)] by simp
qed
qed
text â¹ $\mathbb{B}$ is a standard Borel space. âº
lemma to_bool_measurable:
assumes "f -` {True} â© space M â sets M"
shows "f â M ââ©M bool_borel"
proof(rule measurableI)
fix A
assume h:"A â sets bool_borel"
have h2: "f -` {False} â© space M â sets M"
proof -
have "- {False} = {True}"
by auto
thus ?thesis
by(simp add: vimage_sets_compl_iff[where A="{False}"] assms)
qed
have "A â {True,False}"
by auto
then consider "A = {}" | "A = {True}" | "A = {False}" | "A = {True,False}"
by auto
thus "f -` A â© space M â sets M"
proof cases
case 1
then show ?thesis
by simp
next
case 2
then show ?thesis
by(simp add: assms)
next
case 3
then show ?thesis
by(simp add: h2)
next
case 4
then have "f -` A = f -` {True} ⪠f -` {False}"
by auto
thus ?thesis
using assms h2
by (metis Int_Un_distrib2 sets.Un)
qed
qed simp
interpretation bool : standard_borel_space_UNIV bool_borel
using countable_standard_iff[of bool_borel]
by(auto intro!: standard_borel_space_UNIVI' simp: sets_borel_eq_count_space)
text â¹ $[0,\infty]$ (the set of extended non-negative real numbers) is a standard Borel space. âº
interpretation ennreal : standard_borel_space_UNIV ennreal_borel
proof -
define preal_to_real :: "ennreal â real"
where "preal_to_real â¡ (λr. if r = â then -1
else enn2real r)"
define real_to_preal :: "real â ennreal"
where "real_to_preal â¡ (λr. if r = -1 then â
else ennreal r)"
have preal_to_real_measurable: "preal_to_real â ennreal_borel ââ©M real_borel"
unfolding preal_to_real_def by simp
have real_to_preal_measurable: "real_to_preal â real_borel ââ©M ennreal_borel"
unfolding real_to_preal_def by simp
have preal_real_preal_id: "real_to_preal â preal_to_real = id"
proof
fix r :: ennreal
show "(real_to_preal â preal_to_real) r = id r"
using ennreal_enn2real_if[of r] ennreal_neg
by(auto simp add: real_to_preal_def preal_to_real_def)
qed
show "standard_borel_space_UNIV ennreal_borel"
using standard_borel_space_UNIVI[OF preal_to_real_measurable real_to_preal_measurable preal_real_preal_id]
by simp
qed
subsection â¹ $\mathbb{R}\times\mathbb{R}$ âº
definition real_to_01open :: "real â real" where
"real_to_01open r â¡ arctan r / pi + 1 / 2"
definition real_to_01open_inverse :: "real â real" where
"real_to_01open_inverse r â¡ tan (pi * r - (pi / 2))"
lemma real_to_01open_inverse_correct:
"real_to_01open_inverse â real_to_01open = id"
by(auto simp add: real_to_01open_def real_to_01open_inverse_def distrib_left tan_arctan)
lemma real_to_01open_inverse_correct':
assumes "0 < r" "r < 1"
shows "real_to_01open (real_to_01open_inverse r) = r"
unfolding real_to_01open_def real_to_01open_inverse_def
proof -
have "arctan (tan (pi * r - pi / 2)) = pi * r - pi / 2"
using arctan_unique[of "pi * r - pi / 2"] assms
by simp
hence "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = ((pi * r) - pi / 2)/ pi + 1/2"
by simp
also have "... = r - 1/2 + 1/2"
by (metis (no_types, opaque_lifting) divide_inverse mult.left_neutral nonzero_mult_div_cancel_left pi_neq_zero right_diff_distrib)
finally show "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = r"
by simp
qed
lemma real_to_01open_01 :
"0 < real_to_01open r â§ real_to_01open r < 1"
proof
have "- pi / 2 < arctan r" by(simp add: arctan_lbound)
hence "0 < arctan r + pi / 2" by simp
hence "0 < (1 / pi) * (arctan r + pi / 2)" by simp
thus "0 < real_to_01open r"
by (simp add: add_divide_distrib real_to_01open_def)
next
have "arctan r < pi / 2" using arctan_ubound by simp
hence "arctan r + pi / 2 < pi" by simp
hence "(1 / pi) * (arctan r + pi / 2) < 1" by simp
thus "real_to_01open r < 1"
by(simp add: real_to_01open_def add_divide_distrib)
qed
lemma real_to_01open_continuous:
"continuous_on UNIV real_to_01open"
proof -
have "continuous_on UNIV ((λx. x / pi + 1 / 2) â arctan)"
proof (rule continuous_on_compose)
show "continuous_on UNIV arctan"
by (simp add: continuous_on_arctan)
next
show "continuous_on (range arctan) (λx. x / pi + 1 / 2)"
by(auto intro!: continuous_on_add continuous_on_divide)
qed
thus ?thesis
by(simp add: real_to_01open_def)
qed
lemma real_to_01open_inverse_continuous:
"continuous_on {0<..<1} real_to_01open_inverse"
unfolding real_to_01open_inverse_def
proof(rule Transcendental.continuous_on_tan)
have [simp]: "(λx. pi * x - pi / 2) = (λx. x - pi/2) â (λx. pi * x)"
by auto
have "continuous_on {0<..<1} ..."
proof(rule continuous_on_compose)
show "continuous_on {0<..<1} ((*) pi)"
by simp
next
show "continuous_on ((*) pi ` {0<..<1}) (λx. x - pi / 2)"
using continuous_on_diff[of "(*) pi ` {0<..<1}" "λx. x"]
by simp
qed
thus "continuous_on {0<..<1} (λx. pi * x - pi / 2)" by simp
next
have "ârâ{0<..<1::real}. -(pi/2) < pi * r - pi / 2 â§ pi * r - pi / 2 < pi/2"
by simp
thus "ârâ{0<..<1::real}. cos (pi * r - pi / 2) â 0"
using cos_gt_zero_pi by fastforce
qed
lemma real_to_01open_inverse_measurable:
"real_to_01open_inverse â restrict_space real_borel {0<..<1} ââ©M real_borel"
using borel_measurable_continuous_on_restrict real_to_01open_inverse_continuous
by simp
fun r01_binary_expansion'' :: "real â nat â nat à real à real" where
"r01_binary_expansion'' r 0 = (if 1/2 ⤠r then (1,1 ,1/2)
else (0,1/2, 0))" |
"r01_binary_expansion'' r (Suc n) = (let (_,ur,lr) = r01_binary_expansion'' r n;
k = (ur + lr)/2 in
(if k ⤠r then (1,ur,k)
else (0,k,lr)))"
text â¹ $a_n$ where $r = 0.a_0 a_1 a_2 ....$ for $0 < r < 1$.âº
definition r01_binary_expansion' :: "real â nat â nat" where
"r01_binary_expansion' r n â¡ fst (r01_binary_expansion'' r n)"
text â¹$a_n = 0$ or $1$.âº
lemma real01_binary_expansion'_0or1:
"r01_binary_expansion' r n â {0,1}"
by (cases n) (simp_all add: r01_binary_expansion'_def split_beta' Let_def)
definition r01_binary_sum :: "(nat â nat) â nat â real" where
"r01_binary_sum a n â¡ (âi=0..n. real (a i) * ((1/2)^(Suc i)))"
definition r01_binary_sum_lim :: "(nat â nat) â real" where
"r01_binary_sum_lim â¡ lim â r01_binary_sum"
definition r01_binary_expression :: "real â nat â real" where
"r01_binary_expression â¡ r01_binary_sum â r01_binary_expansion'"
lemma r01_binary_expansion_lr_r_ur:
assumes "0 < r" "r < 1"
shows "(snd (snd (r01_binary_expansion'' r n))) ⤠r â§
r < (fst (snd (r01_binary_expansion'' r n)))"
using assms by (induction n) (simp_all add:split_beta' Let_def)
text â¹â¹0 ⤠lr â§ lr < ur â§ ur ⤠1âº.âº
lemma r01_binary_expansion_lr_ur_nn:
shows "0 ⤠snd (snd (r01_binary_expansion'' r n)) â§
snd (snd (r01_binary_expansion'' r n)) < fst (snd (r01_binary_expansion'' r n)) â§
fst (snd (r01_binary_expansion'' r n)) ⤠1"
by (induction n) (simp_all add:split_beta' Let_def)
lemma r01_binary_expansion_diff:
shows "(fst (snd (r01_binary_expansion'' r n))) - (snd (snd (r01_binary_expansion'' r n))) = (1/2)^(Suc n)"
proof(induction n)
case (Suc n')
then show ?case
proof(cases "r01_binary_expansion'' r n'")
case 1:(fields a ur lr)
assume "fst (snd (r01_binary_expansion'' r n')) - snd (snd (r01_binary_expansion'' r n')) = (1 / 2) ^ (Suc n')"
then have 2:"ur - lr = (1/2)^(Suc n')" by (simp add: 1)
show ?thesis
proof -
have [simp]:"ur * 4 - (ur * 4 + lr * 4) / 2 = (ur - lr) * 2"
by(simp add: division_ring_class.add_divide_distrib)
have "ur * 4 - (ur * 4 + lr * 4) / 2 = (1 / 2) ^ n'"
by(simp add: 2)
moreover have "(ur * 4 + lr * 4) / 2 - lr * 4 = (1 / 2) ^ n'"
by(simp add: division_ring_class.add_divide_distrib ring_class.right_diff_distrib[symmetric] 2)
ultimately show ?thesis
by(simp add: 1 Let_def)
qed
qed
qed simp
text â¹â¹lrn = Snâº.âº
lemma r01_binary_expression_eq_lr:
"snd (snd (r01_binary_expansion'' r n)) = r01_binary_expression r n"
proof(induction n)
case 0
then show ?case
by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def)
next
case 1:(Suc n')
show ?case
proof (cases "r01_binary_expansion'' r n'")
case 2:(fields a ur lr)
then have ih:"lr = (âi = 0..n'. real (fst (r01_binary_expansion'' r i)) * (1 / 2) ^ i / 2)"
using 1 by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def)
have 3:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n'))"
using r01_binary_expansion_diff[of r n'] 2 by simp
show ?thesis
by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def 2 Let_def 3) fact
qed
qed
lemma r01_binary_expression'_sum_range:
"âk::nat. (snd (snd (r01_binary_expansion'' r n))) = real k/2^(Suc n) â§
k < 2^(Suc n) â§
((r01_binary_expansion' r n) = 0 â¶ even k) â§
((r01_binary_expansion' r n) = 1 â¶ odd k)"
proof -
have [simp]:"(snd (snd (r01_binary_expansion'' r n))) = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i)))"
using r01_binary_expression_eq_lr[of r n] by(simp add: r01_binary_expression_def r01_binary_sum_def)
have "âk::nat. (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) = real k/2^(Suc n) â§
k < 2^(Suc n) â§
((r01_binary_expansion' r n) = 0 â¶ even k) â§
((r01_binary_expansion' r n) = 1 â¶ odd k)"
proof(induction n)
case 0
consider "r01_binary_expansion' r 0 = 0" | "r01_binary_expansion' r 0 = 1"
using real01_binary_expansion'_0or1[of r 0] by auto
then show ?case
by cases auto
next
case (Suc n')
then obtain k :: nat where ih:
"(âi = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real k / 2^(Suc n') â§ k < 2^(Suc n')"
by auto
have "(âi = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = (âi = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) + real (r01_binary_expansion' r (Suc n')) * (1 / 2) ^ Suc (Suc n')"
by simp
also have "... = real k / 2^(Suc n') + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')"
proof -
have "âr ra n. (r::real) * (1 / ra) ^ n = r / ra ^ n"
by (simp add: power_one_over)
then show ?thesis
using ih by presburger
qed
also have "... = (2*real k) / 2^(Suc (Suc n')) + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')"
by simp
also have "... = (2*(real k) + real (r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')"
by (simp add: add_divide_distrib)
also have "... = (real (2*k + r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')"
by simp
finally have "(âi = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real (2 * k + r01_binary_expansion' r (Suc n')) / 2 ^ Suc (Suc n')" .
moreover have "2 * k + r01_binary_expansion' r (Suc n') < 2^Suc (Suc n')"
proof -
have "k + 1 ⤠2^Suc n'"
using ih by simp
hence "2*k + 2 ⤠2^Suc (Suc n')"
by simp
thus ?thesis
using real01_binary_expansion'_0or1[of r "Suc n'"]
by auto
qed
moreover have "r01_binary_expansion' r (Suc n') = 0 â¶ even (2 * k + r01_binary_expansion' r (Suc n'))"
by simp
moreover have "r01_binary_expansion' r (Suc n') = 1 â¶ odd (2 * k + r01_binary_expansion' r (Suc n'))"
by simp
ultimately show ?case by fastforce
qed
thus ?thesis
by simp
qed
text â¹â¹an = bn â Sn = S'nâº.âº
lemma r01_binary_expansion'_expression_eq:
"r01_binary_expansion' r1 = r01_binary_expansion' r2 â·
r01_binary_expression r1 = r01_binary_expression r2"
proof
assume "r01_binary_expansion' r1 = r01_binary_expansion' r2"
then show "r01_binary_expression r1 = r01_binary_expression r2"
by(simp add: r01_binary_expression_def)
next
assume "r01_binary_expression r1 = r01_binary_expression r2"
then have 1:"ân. r01_binary_sum (r01_binary_expansion' r1) n = r01_binary_sum (r01_binary_expansion' r2) n"
by(simp add: r01_binary_expression_def)
show "r01_binary_expansion' r1 = r01_binary_expansion' r2"
proof
fix n
show " r01_binary_expansion' r1 n = r01_binary_expansion' r2 n"
proof(cases n)
case 0
then show ?thesis
using 1[of 0] by(simp add: r01_binary_sum_def)
next
fix n'
case (Suc n')
have "r01_binary_sum (r01_binary_expansion' r1) n - r01_binary_sum (r01_binary_expansion' r1) n' = r01_binary_sum (r01_binary_expansion' r2) n - r01_binary_sum (r01_binary_expansion' r2) n'"
by(simp add: 1)
thus ?thesis
using â¹n = Suc n'⺠by(simp add: r01_binary_sum_def)
qed
qed
qed
lemma power2_e:
"âe::real. 0 < e â¹ ân::nat. real_of_rat (1/2)^n < e"
by (simp add: real_arch_pow_inv)
lemma r01_binary_expression_converges_to_r:
assumes "0 < r"
and "r < 1"
shows "LIMSEQ (r01_binary_expression r) r"
proof
fix e :: real
assume "0 < e"
then obtain k :: nat where hk:"real_of_rat (1/2)^k < e"
using power2_e by auto
show "ââ©F x in sequentially. dist (r01_binary_expression r x) r < e"
proof(rule eventually_sequentiallyI[of k])
fix m
assume "k ⤠m"
have "¦ r - r01_binary_expression r m ¦ < e"
proof (cases "r01_binary_expansion'' r m")
case 1:(fields a ur lr)
then have "¦r - r01_binary_expression r m¦ = ¦r - lr¦"
by (metis r01_binary_expression_eq_lr snd_conv)
also have "... = r - lr"
using r01_binary_expansion_lr_r_ur[OF assms] 1
by (metis abs_of_nonneg diff_ge_0_iff_ge snd_conv)
also have "... < e"
proof -
have "r - lr ⤠ur - lr"
using r01_binary_expansion_lr_r_ur[of r] assms 1
by (metis diff_right_mono fst_conv less_imp_le snd_conv)
also have "... = (1/2)^(Suc m)"
using r01_binary_expansion_diff[of r m]
by(simp add: 1)
also have "... ⤠(1/2)^(Suc k)"
using â¹k ⤠m⺠by simp
also have "... < (1/2)^k" by simp
finally show ?thesis
using hk by (simp add: of_rat_divide)
qed
finally show ?thesis .
qed
then show "dist (r01_binary_expression r m) r < e"
by (simp add: dist_real_def)
qed
qed
lemma r01_binary_expression_correct:
assumes "0 < r"
and "r < 1"
shows "r = (ân. real (r01_binary_expansion' r n) * (1/2)^(Suc n))"
proof -
have "(λn. (λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) (Suc n)) = r01_binary_expression r"
proof -
have "ân. {..<Suc n} = {0..n}" by auto
thus ?thesis
by(auto simp add: r01_binary_expression_def r01_binary_sum_def)
qed
hence "LIMSEQ (λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) r"
using r01_binary_expression_converges_to_r[OF assms] LIMSEQ_imp_Suc[of "λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i" r]
by simp
thus ?thesis
using suminf_eq_lim[of "λn. real (r01_binary_expansion' r n) * (1/2)^(Suc n)"] assms limI[of "(λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)" r]
by simp
qed
text â¹â¹S0 ⤠S1 ⤠S2 ⤠...âº.âº
lemma binary_sum_incseq:
"incseq (r01_binary_sum a)"
by(simp add: incseq_Suc_iff r01_binary_sum_def)
lemma r01_eq_iff:
assumes "0 < r1" "r1 < 1"
"0 < r2" "r2 < 1"
shows "r1 = r2 â· r01_binary_expansion' r1 = r01_binary_expansion' r2"
proof auto
assume "r01_binary_expansion' r1 = r01_binary_expansion' r2"
then have 1:"r01_binary_expression r1 = r01_binary_expression r2"
using r01_binary_expansion'_expression_eq[of r1 r2] by simp
have "r1 = lim (r01_binary_expression r1)"
using limI[of _ r1] r01_binary_expression_converges_to_r[of r1] assms(1,2)
by simp
also have "... = lim (r01_binary_expression r2)"
by (simp add: 1)
also have "... = r2"
using limI[of _ r2] r01_binary_expression_converges_to_r[of r2] assms(3,4)
by simp
finally show "r1 = r2" .
qed
lemma power_half_summable:
"summable (λn. ((1::real) / 2) ^ Suc n)"
using power_half_series summable_def by blast
lemma binary_expression_summable:
assumes "ân. a n â {0,1 :: nat}"
shows "summable (λn. real (a n) * (1/2)^(Suc n))"
proof -
have "summable (λn::nat. ¦real (a n) * ((1::real) / (2::real)) ^ Suc n¦)"
proof(rule summable_rabs_comparison_test[of "λn. real (a n) * (1/2)^(Suc n)" "λn. (1/2)^(Suc n)"])
have "ân. ¦real (a n) * (1 / 2) ^ Suc n¦ ⤠(1 / 2)^(Suc n)"
proof -
fix n
have "¦real (a n) * (1 / 2) ^ Suc n¦ = real (a n) * (1 / 2) ^ Suc n"
using assms by simp
also have "... ⤠(1 / 2) ^ Suc n"
proof -
consider "a n = 0" | "a n = 1"
using assms by (meson insertE singleton_iff)
then show ?thesis
by(cases,auto)
qed
finally show "¦real (a n) * (1 / 2) ^ Suc n¦ ⤠(1 / 2)^(Suc n)" .
qed
thus "âN. ânâ¥N. ¦real (a n) * (1 / 2) ^ Suc n¦ ⤠(1 / 2) ^ Suc n"
by simp
next
show "summable (λn. ((1::real) / 2) ^ Suc n)"
using power_half_summable by simp
qed
thus ?thesis by simp
qed
lemma binary_expression_gteq0:
assumes "ân. a n â {0,1 :: nat}"
shows "0 ⤠(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
proof -
have "(ân. 0) ⤠(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] suminf_le[of "λn. 0" "λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k)"] assms
by simp
thus ?thesis by simp
qed
lemma binary_expression_leeq1:
assumes "ân. a n â {0,1 :: nat}"
shows "(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ⤠1"
proof -
have "(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ⤠(ân. (1/2)^(Suc n))"
proof(rule suminf_le)
fix n
have 1:"real (a (n + k)) * (1 / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc (n + k)"
using assms[of "n+k"] by auto
have 2:"((1::real) / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc n"
by simp
show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc n"
by(rule order.trans[OF 1 2])
next
show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] assms
by simp
next
show "summable (λn. ((1::real) / 2) ^ Suc n)"
using power_half_summable by simp
qed
thus ?thesis
using power_half_series sums_unique by fastforce
qed
lemma binary_expression_less_than:
assumes "ân. a n â {0,1 :: nat}"
shows "(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ⤠(ân. (1 / 2) ^ Suc (n + k))"
proof(rule suminf_le)
fix n
show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc (n + k)"
using assms[of "n + k"] by auto
next
show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))"
using summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] binary_expression_summable[of a] assms
by simp
next
show "summable (λn. ((1::real) / 2) ^ Suc (n + k))"
using power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" k]
by simp
qed
lemma lim_sum_ai:
assumes "ân. a n â {0,1 :: nat}"
shows "lim (λn. (âi=0..n. real (a i) * (1/2)^(Suc i))) = (ân::nat. real (a n) * (1/2)^(Suc n))"
proof -
have "ân::nat. {0..n} = {..n}" by auto
hence "LIMSEQ (λn. âi=0..n. real (a i) * (1 / 2) ^ Suc i) (ân. real (a n) * (1 / 2) ^ Suc n)"
using summable_LIMSEQ'[of "λn. real (a n) * (1/2)^(Suc n)"] binary_expression_summable[of a] assms
by simp
thus "lim (λn. (âi=0..n. real (a i) * (1/2)^(Suc i))) = (ân. real (a n) * (1 / 2) ^ Suc n)"
using limI by simp
qed
lemma half_1_minus_sum:
"1 - (âi<k. ((1::real) / 2) ^ Suc i) = (1/2)^k"
by(induction k) auto
lemma half_sum:
"(ân. ((1::real) / 2) ^ (Suc (n + k))) = (1/2)^k"
using suminf_split_initial_segment[of "λn. ((1::real) / 2) ^ (Suc n)" k] half_1_minus_sum[of k] power_half_series sums_unique[of "λn. (1 / 2) ^ Suc n" 1] power_half_summable
by fastforce
lemma ai_exists0_less_than_sum:
assumes "ân. a n â {0,1}"
"i ⥠m"
and "a i = 0"
shows "(ân::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) < (1 / 2) ^ m"
proof -
have "(ân::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) = (ân<i-m. real (a (n + m)) * (1/2)^(Suc (n + m))) + (ân::nat. real (a (n + i)) * (1/2)^(Suc (n + i)))"
using suminf_split_initial_segment[of "λn. real (a (n + m)) * (1/2)^(Suc (n + m))" "i-m"] assms(1) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" m] assms(2)
by simp
also have "... < (1 / 2) ^ m"
proof -
have "(ân. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ⤠(1 / 2) ^ Suc i"
proof -
have "(ân::nat. real (a (n + i)) * (1/2)^(Suc (n + i))) = (ân::nat. real (a (Suc n + i)) * (1/2)^(Suc (Suc n + i)))"
using suminf_split_head[of "λn. real (a (n + i)) * (1/2)^(Suc (n + i))"] assms(1,3) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i]
by simp
also have "... = (ân::nat. real (a (n + Suc i)) * (1/2)^(Suc n + Suc i))"
by simp
also have "... ⤠(ân::nat. (1/2)^(Suc n + Suc i))"
using binary_expression_less_than[of a "Suc i"] assms(1)
by simp
also have "... = (1/2)^(Suc i)"
using half_sum[of "Suc i"] by simp
finally show ?thesis .
qed
moreover have "(ân<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ⤠(1/2)^m - (1/2)^i"
proof -
have "(ân<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ⤠(ân<i - m. (1 / 2) ^ Suc (n + m))"
proof -
have "real (a i) * (1 / 2) ^ Suc i ⤠(1 / 2) ^ Suc i" for i
using assms(1)[of i] by auto
thus ?thesis
by (simp add: sum_mono)
qed
also have "... = (ân. (1 / 2) ^ Suc (n + m)) - (ân. (1 / 2) ^ Suc (n + (i - m) + m))"
using suminf_split_initial_segment[of "λn. (1 / 2) ^ Suc (n + m)" "i-m"] power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" m]
by fastforce
also have "... = (ân. (1 / 2) ^ Suc (n + m)) - (ân. (1 / 2) ^ Suc (n + i))"
using assms(2) by simp
also have "... = (1/2)^m - (1/2)^i"
using half_sum by fastforce
finally show ?thesis .
qed
ultimately have "(ân<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) + (ân. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ⤠(1 / 2) ^ Suc i + (1 / 2) ^ m - (1 / 2) ^ i"
by linarith
also have "... < (1 / 2) ^ m "
by simp
finally show ?thesis .
qed
finally show ?thesis .
qed
lemma ai_exists0_less_than1:
assumes "ân. a n â {0,1}"
and "âi. a i = 0"
shows "(ân::nat. real (a n) * (1/2)^(Suc n)) < 1"
using ai_exists0_less_than_sum[of a 0] assms
by auto
lemma ai_1_gt:
assumes "ân. a n â {0,1}"
and "a i = 1"
shows "(1/2)^(Suc i) ⤠(ân::nat. real (a (n+i)) * (1/2)^(Suc (n+i)))"
proof -
have 1:"(ân::nat. real (a (n+i)) * (1/2)^(Suc (n+i))) = (1 / 2) ^ Suc (0 + i) + (ân. real (a (Suc n + i)) * (1 / 2) ^ Suc (Suc n + i))"
using suminf_split_head[of "λn. real (a (n+i)) * (1/2)^(Suc (n+i))"] binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i] assms
by simp
show ?thesis
using 1 binary_expression_gteq0[of a "Suc i"] assms(1)
by simp
qed
lemma ai_exists1_gt0:
assumes "ân. a n â {0,1}"
and "âi. a i = 1"
shows "0 < (ân::nat. real (a n) * (1/2)^(Suc n))"
proof -
obtain k where h1: "a k = 1"
using assms(2) by auto
have "(1/2)^(Suc k) = (ân::nat. (if n = k then (1/2)^(Suc k) else (0::real)))"
proof -
have "(λn. if n â {k} then (1 / 2) ^ Suc k else (0::real)) = (λn. if n = k then (1/2)^(Suc k) else 0)"
by simp
moreover have "(λn. if n â {k} then (1 / 2) ^ Suc k else (0::real)) sums (ârâ{k}. (1 / 2) ^ Suc k)"
using sums_If_finite_set[of "{k}" "λn. ((1::real)/2)^(Suc k)"] by simp
ultimately have "(λn. if n = k then (1 / 2) ^ Suc k else (0::real)) sums (1/2)^(Suc k)"
by simp
thus ?thesis
using sums_unique[of "λn. if n = k then (1 / 2) ^ Suc k else (0::real)" "(1/2)^(Suc k)"]
by simp
qed
also have "(ân::nat. (if n = k then (1/2)^(Suc k) else 0)) ⤠(ân::nat. real (a n) * (1/2)^(Suc n))"
proof(rule suminf_le)
show "ân. (if n = k then (1 / 2) ^ Suc k else 0) ⤠real (a n) * (1 / 2) ^ Suc n"
proof -
fix n
show "(if n = k then (1 / 2) ^ Suc k else 0) ⤠real (a n) * (1 / 2) ^ Suc n"
by(cases "n = k"; simp add: h1)
qed
next
show "summable (λn. if n = k then (1 / 2) ^ Suc k else (0::real))"
using summable_single[of k "λn. ((1::real) / 2) ^ Suc k"]
by simp
next
show "summable (λn. real (a n) * (1 / 2) ^ Suc n)"
using binary_expression_summable[of a] assms(1)
by simp
qed
finally have "(1 / 2) ^ Suc k ⤠(ân. real (a n) * (1 / 2) ^ Suc n)" .
moreover have "0 < ((1::real) / 2) ^ Suc k" by simp
ultimately show ?thesis by linarith
qed
lemma r01_binary_expression_ex0:
assumes "0 < r" "r < 1"
shows "âi. r01_binary_expansion' r i = 0"
proof (rule ccontr)
assume "¬ (â i. r01_binary_expansion' r i = 0)"
then have "âi. r01_binary_expansion' r i = 1"
using real01_binary_expansion'_0or1[of r] by blast
hence 1:"r01_binary_expression r = (λn. âi=0..n. ((1/2)^(Suc i)))"
by(auto simp: r01_binary_expression_def r01_binary_sum_def)
have "LIMSEQ (r01_binary_expression r) 1"
proof -
have "LIMSEQ (λn. âi=0..n. (((1::real)/2)^(Suc i))) 1"
using power_half_series sums_def'[of "λn. ((1::real)/2)^(Suc n)" 1]
by simp
thus ?thesis
using 1 by simp
qed
moreover have "LIMSEQ (r01_binary_expression r) r"
using r01_binary_expression_converges_to_r[of r] assms
by simp
ultimately have "r = 1"
using LIMSEQ_unique by auto
thus False
using assms by simp
qed
lemma r01_binary_expression_ex1:
assumes "0 < r" "r < 1"
shows "âi. r01_binary_expansion' r i = 1"
proof (rule ccontr)
assume "¬ (âi. r01_binary_expansion' r i = 1)"
then have "âi. r01_binary_expansion' r i = 0"
using real01_binary_expansion'_0or1[of r] by blast
hence 1:"r01_binary_expression r = (λn. âi=0..n. 0)"
by(auto simp add: r01_binary_expression_def r01_binary_sum_def)
hence "LIMSEQ (r01_binary_expression r) 0"
by simp
moreover have "LIMSEQ (r01_binary_expression r) r"
using r01_binary_expression_converges_to_r[of r] assms
by simp
ultimately have "r = 0"
using LIMSEQ_unique by auto
thus False
using assms by simp
qed
lemma r01_binary_expansion'_gt1:
"1 ⤠r â· (ân. r01_binary_expansion' r n = 1)"
proof auto
fix n
assume h:"1 ⤠r"
show "r01_binary_expansion' r n = Suc 0"
unfolding r01_binary_expansion'_def
proof(cases n)
case 0
then show "fst (r01_binary_expansion'' r n) = Suc 0"
using h by simp
next
case 2:(Suc n')
show "fst (r01_binary_expansion'' r n) = Suc 0"
proof(cases "r01_binary_expansion'' r n'")
case 3:(fields a ur lr)
then have "(ur + lr) / 2 ⤠1"
using r01_binary_expansion_lr_ur_nn[of r "Suc n'"]
by (cases "((ur + lr) / 2) ⤠r") (auto simp: Let_def)
thus "fst (r01_binary_expansion'' r n) = Suc 0"
using h by(simp add: 2 3 Let_def)
qed
qed
next
assume h:"ân. r01_binary_expansion' r n = Suc 0"
show "1 ⤠r"
proof(rule ccontr)
assume "¬ 1 ⤠r"
then consider "r ⤠0" | "0 < r ⧠r < 1"
by linarith
then show "False"
proof cases
case 1
then have "r01_binary_expansion' r 0 = 0"
by(simp add: r01_binary_expansion'_def)
then show ?thesis
using h by simp
next
case 2
then have "âi. r01_binary_expansion' r i = 0"
using r01_binary_expression_ex0[of r] by simp
then show ?thesis
using h by simp
qed
qed
qed
lemma r01_binary_expansion'_lt0:
"r ⤠0 â· (ân. r01_binary_expansion' r n = 0)"
proof auto
fix n
assume h:"r ⤠0"
show "r01_binary_expansion' r n = 0"
proof(cases n)
case 0
then show ?thesis
using h by(simp add: r01_binary_expansion'_def)
next
case hn:(Suc n')
then show ?thesis
unfolding r01_binary_expansion'_def
proof(cases "r01_binary_expansion'' r n'")
case 1:(fields a ur lr)
then have "0 < ((ur + lr) / 2)"
using r01_binary_expansion_lr_ur_nn[of r n']
by simp
hence "r < ..."
using h by linarith
then show "fst (r01_binary_expansion'' r n) = 0 "
by(simp add: 1 hn Let_def)
qed
qed
next
assume h:"ân. r01_binary_expansion' r n = 0"
show "r ⤠0"
proof(rule ccontr)
assume "¬ r ⤠0"
then consider "0 < r ⧠r < 1" | "1 ⤠r" by linarith
thus False
proof cases
case 1
then have "âi. r01_binary_expansion' r i = 1"
using r01_binary_expression_ex1[of r] by simp
then show ?thesis
using h by simp
next
case 2
then show ?thesis
using r01_binary_expansion'_gt1[of r] h by simp
qed
qed
qed
text â¹The sequence $111111\dots$ does not appear in $r = 0.a_1 a_2\dots$. âº
lemma r01_binary_expression_ex0_strong:
assumes "0 < r" "r < 1"
shows "âiâ¥n. r01_binary_expansion' r i = 0"
proof(cases "r01_binary_expansion'' r n")
case 1:(fields a ur lr)
show ?thesis
proof(rule ccontr)
assume "¬ (âiâ¥n. r01_binary_expansion' r i = 0)"
then have h:"âiâ¥n. r01_binary_expansion' r i = 1"
using real01_binary_expansion'_0or1[of r] by blast
have "r = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (âi::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))"
proof -
have "r = (âl. real (r01_binary_expansion' r l) * (1 / 2) ^ Suc l)"
using r01_binary_expression_correct[of r] assms by simp
also have "... = (âl. real (r01_binary_expansion' r (l + Suc n)) * (1 / 2) ^ Suc (l + Suc n)) + (âi<Suc n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)"
apply(rule suminf_split_initial_segment)
apply(rule binary_expression_summable)
using real01_binary_expansion'_0or1[of r] by simp
also have "... = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (âi::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))"
proof -
have "ân. {..<Suc n} = {0..n}" by auto
thus ?thesis by simp
qed
finally show ?thesis .
qed
also have "... = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (âi::nat. ((1/2)^(Suc (i + (Suc n)))))"
using h by simp
also have "... = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (1/2)^(Suc n)"
using half_sum[of "Suc n"] by simp
also have "... = lr + (1/2)^(Suc n)"
using 1 r01_binary_expression_eq_lr[of r n]
by(simp add: r01_binary_expression_def r01_binary_sum_def)
also have "... = ur"
using r01_binary_expansion_diff[of r n]
by(simp add: 1)
finally have "r = ur" .
moreover have "r < ur"
using r01_binary_expansion_lr_r_ur[of r n] assms 1
by simp
ultimately show False
by simp
qed
qed
text â¹ A binary expression is well-formed when $111\dots$ does not appear in the tail of the sequence âº
definition biexp01_well_formed :: "(nat â nat) â bool" where
"biexp01_well_formed a â¡ (ân. a n â {0,1}) â§ (ân. âmâ¥n. a m = 0)"
lemma biexp01_well_formedE:
assumes "biexp01_well_formed a"
shows "(ân. a n â {0,1}) â§ (ân. âmâ¥n. a m = 0)"
using assms by(simp add: biexp01_well_formed_def)
lemma biexp01_well_formedI:
assumes "ân. a n â {0,1}"
and "ân. âmâ¥n. a m = 0"
shows "biexp01_well_formed a"
using assms by(simp add: biexp01_well_formed_def)
lemma r01_binary_expansion_well_formed:
assumes "0 < r" "r < 1"
shows "biexp01_well_formed (r01_binary_expansion' r)"
using r01_binary_expression_ex0_strong[of r] assms real01_binary_expansion'_0or1[of r]
by(simp add: biexp01_well_formed_def)
lemma biexp01_well_formed_comb:
assumes "biexp01_well_formed a"
and "biexp01_well_formed b"
shows "biexp01_well_formed (λn. if even n then a (n div 2)
else b ((n-1) div 2))"
proof(rule biexp01_well_formedI)
show "ân. (if even n then a (n div 2) else b ((n - 1) div 2)) â {0, 1}"
using assms biexp01_well_formedE by simp
next
fix n
obtain m where 1:"mâ¥n â§ a m = 0"
using assms biexp01_well_formedE by blast
then have "a ((2*m) div 2) = 0" by simp
hence "(if even (2*m) then a (2*m div 2) else b ((2*m - 1) div 2)) = 0"
by simp
moreover have "2*m ⥠n" using 1 by simp
ultimately show "âmâ¥n. (if even m then a (m div 2) else b ((m - 1) div 2)) = 0"
by auto
qed
lemma nat_complete_induction:
assumes "P (0 :: nat)"
and "ân. (âm. m ⤠n â¹ P m) â¹ P (Suc n)"
shows "P n"
proof(cases n)
case 0
then show ?thesis
using assms(1) by simp
next
case h:(Suc n')
have "P (Suc n')"
proof(rule assms(2))
show "âm. m ⤠n' â¹ P m"
proof(induction n')
case 0
then show ?case
using assms(1) by simp
next
case (Suc n'')
then show ?case
by (metis assms(2) le_SucE)
qed
qed
thus ?thesis
using h by simp
qed
text â¹ â¹(âm. real (a m) * (1 / 2) ^ Suc m) n = a nâº.âº
lemma biexp01_well_formed_an:
assumes "biexp01_well_formed a"
shows "r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) n = a n"
proof(rule nat_complete_induction[of _ n])
show "r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) 0 = a 0"
proof (auto simp add: r01_binary_expansion'_def)
assume h:"1 ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2"
show "Suc 0 = a 0"
proof(rule ccontr)
assume "Suc 0 â a 0"
then have "a 0 = 0"
using assms(1) biexp01_well_formedE[of a] by auto
hence "(âm. real (a m) * (1 / 2) ^ (Suc m)) = (âm. real (a (Suc m)) * (1 / 2) ^ (Suc (Suc m)))"
using suminf_split_head[of "λm. real (a m) * (1 / 2) ^ (Suc m)"] binary_expression_summable[of a] assms biexp01_well_formedE
by simp
also have "... < 1/2"
using ai_exists0_less_than_sum[of a 1] assms biexp01_well_formedE[of a]
by auto
finally have "(âm. real (a m) * (1 / 2) ^ m / 2) < 1/2"
by simp
thus False
using h by simp
qed
next
assume h:"¬ 1 ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2"
show "a 0 = 0"
proof(rule ccontr)
assume "a 0 â 0"
then have "a 0 = 1"
using assms(1) biexp01_well_formedE[of a]
by (meson insertE singletonD)
hence "1/2 ⤠(âm. real (a m) * (1 / 2) ^ (Suc m))"
using ai_1_gt[of a 0] assms(1) biexp01_well_formedE[of a]
by auto
thus False
using h by simp
qed
qed
next
fix n :: nat
assume ih:"(âm. m ⤠n â¹ r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) m = a m)"
show "r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) (Suc n) = a (Suc n)"
proof(cases "r01_binary_expansion'' (âm. real (a m) * (1 / 2) ^ Suc m) n")
case h:(fields bn ur lr)
then have hlr:"lr = (âk=0..n. real (a k) * (1 / 2) ^ Suc k)"
using r01_binary_expression_eq_lr[of "âm. real (a m) * (1 / 2) ^ Suc m" n] ih
by(simp add: r01_binary_expression_def r01_binary_sum_def)
have hlr2:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))"
proof -
have "(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))"
using r01_binary_expansion_diff[of "âm. real (a m) * (1 / 2) ^ Suc m" n] h by simp
show ?thesis
by (simp add: â¹(ur + lr) / 2 = lr + (1 / 2) ^ Suc (Suc n)⺠of_rat_add of_rat_divide of_rat_power)
qed
show ?thesis
using h
proof(auto simp add: r01_binary_expansion'_def Let_def)
assume h1: "(ur + lr) ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2"
show "Suc 0 = a (Suc n)"
proof(rule ccontr)
assume "Suc 0 â a (Suc n)"
then have "a (Suc n) = 0"
using assms(1) biexp01_well_formedE[of a] by auto
have "(âm. real (a m) * (1 / 2) ^ m / 2) < (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n))"
proof -
have "(âm. real (a m) * (1 / 2) ^ (Suc m)) = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))"
proof -
have "{0..n} = {..<Suc n}" by auto
thus ?thesis
using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a]
by simp
qed
also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n))"
using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] â¹a (Suc n) = 0âº
by simp
also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + Suc (Suc n)))"
by simp
also have "... < (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^Suc (Suc n)"
using ai_exists0_less_than_sum[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a]
by auto
finally show ?thesis by simp
qed
thus False
using h1 hlr2 hlr by simp
qed
next
assume h2:"¬ ur + lr ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2"
show "a (Suc n) = 0"
proof(rule ccontr)
assume "a (Suc n) â 0"
then have "a (Suc n) = 1"
using biexp01_well_formedE[OF assms(1)]
by (meson insertE singletonD)
have "(âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n)) ⤠(âm. real (a m) * (1 / 2) ^ m / 2)"
proof -
have "(âm. real (a m) * (1 / 2) ^ (Suc m)) = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))"
proof -
have "{0..n} = {..<Suc n}" by auto
thus ?thesis
using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a]
by simp
qed
also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n)) + (1 / 2) ^ Suc (Suc n)"
using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] â¹a (Suc n) = 1âº
by simp
also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + (Suc (Suc n)))) + (1 / 2) ^ Suc (Suc n)"
by simp
also have "... ⥠(âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1 / 2) ^ Suc (Suc n)"
using binary_expression_gteq0[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a] by simp
finally show ?thesis by simp
qed
thus False
using h2 hlr2 hlr by simp
qed
qed
qed
qed
lemma f01_borel_measurable:
assumes "f -` {0::real} â sets real_borel"
"f -` {1} â sets borel"
and "âr::real. f r â {0,1}"
shows "f â borel_measurable real_borel"
proof(rule measurableI)
fix U :: "real set"
assume "U â sets borel"
consider "1 â U â§ 0 â U" | "1 â U â§ 0 â U" | "1 â U â§ 0 â U" | "1 â U â§ 0 â U"
by auto
then show "f -` U â© space real_borel â sets borel"
proof cases
case 1
then have "f -` U = UNIV"
using assms(3) by auto
then show ?thesis by simp
next
case 2
then have "f -` U = f -` {1}"
using assms(3) by fastforce
then show ?thesis
using assms(2) by simp
next
case 3
then have "f -` U = f -` {0}"
using assms(3) by fastforce
then show ?thesis
using assms(1) by simp
next
case 4
then have "f -` U = {}"
using assms(3) by (metis all_not_in_conv insert_iff vimage_eq)
then show ?thesis by simp
qed
qed simp
lemma r01_binary_expansion'_measurable:
"(λr. real (r01_binary_expansion' r n)) â borel_measurable (borel :: real measure)"
proof -
have "(λr. real (r01_binary_expansion' r n)) -`{0} â sets borel â§ (λr. real (r01_binary_expansion' r n)) -`{1} â sets borel"
proof -
let ?A = "{..0::real} ⪠(âiâ{l::nat. l < 2^(Suc n) â§ even l} . {i/2^(Suc n)..<(Suc i)/2^(Suc n)})"
let ?B = "{1::real..} ⪠(âiâ{l::nat. l < 2^(Suc n) â§ odd l} . {i/2^(Suc n)..<(Suc i)/2^(Suc n)})"
have "?A â sets borel" by simp
have "?B â sets borel" by simp
have hE:"?A â© ?B = {}"
proof auto
fix r :: real
fix l :: nat
assume h: "r ⤠0"
"odd l"
"real l / (2 * 2 ^ n) ⤠r"
then have "0 < l" by(cases l; auto)
hence "0 < real l / (2 * 2 ^ n)" by simp
thus False
using h by simp
next
fix r :: real
fix l :: nat
assume h: "l < 2 * 2 ^ n"
"even l"
"1 ⤠r"
"r < (1 + real l) / (2 * 2 ^ n)"
then have "1 + real l ⤠2 * 2 ^ n"
by (simp add: nat_less_real_le)
moreover have "1 + real l â 2 * 2 ^ n"
using h by auto
ultimately have "1 + real l < 2 * 2 ^ n" by simp
hence "(1 + real l) / (2 * 2 ^ n) < 1" by simp
thus False using h by linarith
next
fix r :: real
fix l1 l2 :: nat
assume h: "even l1" "odd l2"
"real l1 / (2 * 2 ^ n) ⤠r" "r < (1 + real l1) / (2 * 2 ^ n)"
"real l2 / (2 * 2 ^ n) ⤠r" "r < (1 + real l2) / (2 * 2 ^ n)"
then consider "l1 < l2" | "l2 < l1" by fastforce
thus False
proof cases
case 1
then have "(1 + real l1) / (2 * 2 ^ n) ⤠real l2 / (2 * 2 ^ n)"
by (simp add: frac_le)
then show ?thesis
using h by simp
next
case 2
then have "(1 + real l2) / (2 * 2 ^ n) ⤠real l1 / (2 * 2 ^ n)"
by (simp add: frac_le)
then show ?thesis
using h by simp
qed
qed
have hU:"?A ⪠?B = UNIV"
proof
show "?A ⪠?B â UNIV" by simp
next
show "UNIV â ?A ⪠?B"
proof
fix r :: real
consider "r ⤠0" | "0 < r ⧠r < 1" | "1 ⤠r" by linarith
then show "r â ?A ⪠?B"
proof cases
case 1
then show ?thesis by simp
next
case 2
show ?thesis
proof(cases "r01_binary_expansion'' r n")
case hc:(fields a ur lr)
then have hlu:"lr ⤠r ⧠r < ur"
using 2 r01_binary_expansion_lr_r_ur[of r n] by simp
obtain k :: nat where hk:
"lr = real k / 2 ^ Suc n â§ k < 2 ^ Suc n"
using r01_binary_expression'_sum_range[of r n] hc
by auto
hence "ur = real (Suc k) / 2^Suc n"
using r01_binary_expansion_diff[of r n] hc
by (simp add: add_divide_distrib power_one_over)
thus ?thesis
using hlu hk by auto
qed
next
case 3
then show ?thesis by simp
qed
qed
qed
have hi1:"- ?A = ?B"
proof -
have "?B â - ?A"
using hE by blast
moreover have "-?A â ?B"
proof -
have "-(?A ⪠?B) = {}"
using hU by simp
hence "(-?A) â© (-?B) = {}" by simp
thus ?thesis
by blast
qed
ultimately show ?thesis
by blast
qed
have hi2: "?A = -?B"
using hi1 by blast
let ?U0 = "(λr. real (r01_binary_expansion' r n)) -`{0}"
let ?U1 = "(λr. real (r01_binary_expansion' r n)) -`{1}"
have hU':"?U0 ⪠?U1 = UNIV"
proof -
have "?U0 ⪠?U1 = (λr. real (r01_binary_expansion' r n)) -`{0,1}"
by auto
thus ?thesis
using real01_binary_expansion'_0or1[of _ n] by auto
qed
have hE':"?U0 â© ?U1 = {}"
by auto
have hiu1:"- ?U0 = ?U1"
using hE' hU' by fastforce
have hiu2:"- ?U1 = ?U0"
using hE' hU' by fastforce
have "?U0 â ?A"
proof
fix r
assume "r â ?U0"
then have h1:"r01_binary_expansion' r n = 0"
by simp
then consider "r ⤠0" | "0 < r ⧠r < 1"
using r01_binary_expansion'_gt1[of r] by fastforce
thus "r â ?A"
proof cases
case 1
then show ?thesis by simp
next
case 2
then have 3:"(snd (snd (r01_binary_expansion'' r n))) ⤠r â§
r < (fst (snd (r01_binary_expansion'' r n)))"
using r01_binary_expansion_lr_r_ur[of r n] by simp
obtain k where 4:
"(snd (snd (r01_binary_expansion'' r n))) =
real k / 2 ^ Suc n â§
k < 2 ^ Suc n â§ even k"
using r01_binary_expression'_sum_range[of r n] h1
by auto
have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n"
proof -
have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n"
using r01_binary_expansion_diff[of r n] by linarith
thus ?thesis
using 4
by (simp add: add_divide_distrib power_one_over)
qed
thus ?thesis
using 3 4 by auto
qed
qed
have "?U1 â ?B"
proof
fix r
assume "r â ?U1"
then have h1:"r01_binary_expansion' r n = 1"
by simp
then consider "1 ⤠r" | "0 < r ⧠r < 1"
using r01_binary_expansion'_lt0[of r] by fastforce
thus "r â ?B"
proof cases
case 1
then show ?thesis by simp
next
case 2
then have 3:"(snd (snd (r01_binary_expansion'' r n))) ⤠r â§
r < (fst (snd (r01_binary_expansion'' r n)))"
using r01_binary_expansion_lr_r_ur[of r n] by simp
obtain k where 4:
"(snd (snd (r01_binary_expansion'' r n))) =
real k / 2 ^ Suc n â§
k < 2 ^ Suc n â§ odd k"
using StandardBorel.r01_binary_expression'_sum_range[of r n] h1
by auto
have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n"
proof -
have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n"
using r01_binary_expansion_diff[of r n] by simp
thus ?thesis
using 4
by (simp add: add_divide_distrib power_one_over)
qed
thus ?thesis
using 3 4 by auto
qed
qed
have "?U0 = ?A"
proof
show "?U0 â ?A" by fact
next
show "?A â ?U0"
using â¹?U1 â ?B⺠Compl_subset_Compl_iff[of ?U0 ?A] hi1 hiu1
by blast
qed
have "?U1 = ?B"
using �U0 = ?A⺠hi1 hiu1 by auto
show ?thesis
using â¹?U0 = ?A⺠â¹?U1 = ?B⺠â¹?A â sets borel⺠â¹?B â sets borelâº
by simp
qed
thus ?thesis
using f01_borel_measurable[of "(λr. real (r01_binary_expansion' r n))"] real01_binary_expansion'_0or1[of _ n]
by simp
qed
definition r01_to_r01_r01_fst' :: "real â nat â nat" where
"r01_to_r01_r01_fst' r n â¡ r01_binary_expansion' r (2*n)"
lemma r01_to_r01_r01_fst'in01:
"ân. r01_to_r01_r01_fst' r n â {0,1}"
using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_fst'_def)
definition r01_to_r01_r01_fst_sum :: "real â nat â real" where
"r01_to_r01_r01_fst_sum â¡ r01_binary_sum â r01_to_r01_r01_fst'"
definition r01_to_r01_r01_fst :: "real â real" where
"r01_to_r01_r01_fst = lim â r01_to_r01_r01_fst_sum"
lemma r01_to_r01_r01_fst_def':
"r01_to_r01_r01_fst r = (ân. real (r01_binary_expansion' r (2*n)) * (1/2)^(n+1))"
proof -
have "r01_to_r01_r01_fst_sum r = (λn. âi=0..n. real (r01_binary_expansion' r (2*i)) * (1/2)^(i+1))"
by(auto simp add: r01_to_r01_r01_fst_sum_def r01_binary_sum_def r01_to_r01_r01_fst'_def)
thus ?thesis
using lim_sum_ai real01_binary_expansion'_0or1
by(simp add: r01_to_r01_r01_fst_def)
qed
lemma r01_to_r01_r01_fst_measurable:
"r01_to_r01_r01_fst â borel_measurable borel"
unfolding r01_to_r01_r01_fst_def'
using r01_binary_expansion'_measurable by auto
definition r01_to_r01_r01_snd' :: "real â nat â nat" where
"r01_to_r01_r01_snd' r n = r01_binary_expansion' r (2*n + 1)"
lemma r01_to_r01_r01_snd'in01:
"ân. r01_to_r01_r01_snd' r n â {0,1}"
using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_snd'_def)
definition r01_to_r01_r01_snd_sum :: "real â nat â real" where
"r01_to_r01_r01_snd_sum â¡ r01_binary_sum â r01_to_r01_r01_snd'"
definition r01_to_r01_r01_snd :: "real â real" where
"r01_to_r01_r01_snd = lim â r01_to_r01_r01_snd_sum"
lemma r01_to_r01_r01_snd_def':
"r01_to_r01_r01_snd r = (ân. real (r01_binary_expansion' r (2*n + 1)) * (1/2)^(n+1))"
proof -
have "r01_to_r01_r01_snd_sum r = (λn. âi=0..n. real (r01_binary_expansion' r (2*i + 1)) * (1/2)^(i+1))"
by(auto simp add: r01_to_r01_r01_snd_sum_def r01_binary_sum_def r01_to_r01_r01_snd'_def)
thus ?thesis
using lim_sum_ai real01_binary_expansion'_0or1
by(simp add: r01_to_r01_r01_snd_def)
qed
lemma r01_to_r01_r01_snd_measurable:
"r01_to_r01_r01_snd â borel_measurable borel"
unfolding r01_to_r01_r01_snd_def'
using r01_binary_expansion'_measurable by auto
definition r01_to_r01_r01 :: "real â real à real" where
"r01_to_r01_r01 r = (r01_to_r01_r01_fst r,r01_to_r01_r01_snd r)"
lemma r01_to_r01_r01_image:
"r01_to_r01_r01 r â {0..1}Ã{0..1}"
using r01_to_r01_r01_fst_def'[of r] r01_to_r01_r01_snd_def'[of r] real01_binary_expansion'_0or1
binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n+1)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n+1)" 0]
by(simp add: r01_to_r01_r01_def)
lemma r01_to_r01_r01_measurable:
"r01_to_r01_r01 â real_borel ââ©M real_borel â¨â©M real_borel"
unfolding r01_to_r01_r01_def
using borel_measurable_Pair[of r01_to_r01_r01_fst borel r01_to_r01_r01_snd] r01_to_r01_r01_fst_measurable r01_to_r01_r01_snd_measurable
by(simp add: borel_prod)
lemma r01_to_r01_r01_3over4:
"r01_to_r01_r01 (3/4) = (1/2,1/2)"
proof -
have h0:"r01_binary_expansion' (3/4) 0 = 1"
by (simp add: r01_binary_expansion'_def)
have h1:"r01_binary_expansion' (3/4) 1 = 1"
by (simp add: r01_binary_expansion'_def Let_def of_rat_divide)
have hn:"ân. n>1â¹ r01_binary_expansion' (3/4) n = 0"
proof -
fix n :: nat
assume h:"1 < n"
show "r01_binary_expansion' (3 / 4) n = 0"
proof(rule ccontr)
assume "r01_binary_expansion' (3 / 4) n â 0"
have "3/4 < (âi=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
proof -
have "(âi=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (âi=(Suc 0)..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
by(rule sum.atLeast_Suc_atMost) (simp add: h)
also have "... = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (real (r01_binary_expansion' (3/4) 1) * (1/2)^(Suc 1) + (âi=(Suc (Suc 0))..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)))"
using sum.atLeast_Suc_atMost[OF order.strict_implies_order[OF h],of "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"]
by simp
also have "... = 3/4 + (âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
using h0 h1 by(simp add: numeral_2_eq_2)
also have "... > 3/4"
proof -
have "(âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = (âi=2..n-1. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) + real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n"
by (metis (no_types, lifting) h One_nat_def Suc_pred less_2_cases_iff less_imp_add_positive order_less_irrefl plus_1_eq_Suc sum.cl_ivl_Suc zero_less_Suc)
hence "real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n ⤠(âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
using ordered_comm_monoid_add_class.sum_nonneg[of "{2..n-1}" "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"]
by simp
moreover have "0 < real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n"
using â¹r01_binary_expansion' (3 / 4) n â 0⺠by simp
ultimately have "0 < (âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))"
by simp
thus ?thesis by simp
qed
finally show "3 / 4 < (âi = 0..n. real (r01_binary_expansion' (3 / 4) i) * (1 / 2) ^ Suc i)" .
qed
moreover have "(âi=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) ⤠3/4"
using r01_binary_expansion_lr_r_ur[of "3/4" n] r01_binary_expression_eq_lr[of "3/4" n]
by(simp add: r01_binary_expression_def r01_binary_sum_def)
ultimately show False by simp
qed
qed
show ?thesis
proof
have "fst (r01_to_r01_r01 (3 / 4)) = (ân. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n)"
by(simp add: r01_to_r01_r01_def r01_to_r01_r01_fst_def')
also have "... = 1/2 + (ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n))"
using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n)"] real01_binary_expansion'_0or1[of "3/4"] h0
by simp
also have "... = 1/2"
proof -
have "ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n) = 0"
using hn by simp
hence "(ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n)) = 0"
by simp
thus ?thesis
by simp
qed
finally show "fst (r01_to_r01_r01 (3 / 4)) = fst (1 / 2, 1 / 2)"
by simp
next
have "snd (r01_to_r01_r01 (3 / 4)) = (ân. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n)"
by(simp add: r01_to_r01_r01_def r01_to_r01_r01_snd_def')
also have "... = 1/2 + (ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n))"
using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n + 1)"] real01_binary_expansion'_0or1[of "3/4"] h1
by simp
also have "... = 1/2"
proof -
have "ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n) = 0"
using hn by simp
hence "(ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n)) = 0"
by simp
thus ?thesis
by simp
qed
finally show "snd (r01_to_r01_r01 (3 / 4)) = snd (1 / 2, 1 / 2)"
by simp
qed
qed
definition r01_r01_to_r01' :: "real à real â nat â nat" where
"r01_r01_to_r01' rs ⡠(λn. if even n then r01_binary_expansion' (fst rs) (n div 2)
else r01_binary_expansion' (snd rs) ((n-1) div 2))"
lemma r01_r01_to_r01'in01:
"ân. r01_r01_to_r01' rs n â {0,1}"
using real01_binary_expansion'_0or1 by (simp add: r01_r01_to_r01'_def)
lemma r01_r01_to_r01'_well_formed:
assumes "0 < r1" "r1 < 1"
and "0 < r2" "r2 < 1"
shows "biexp01_well_formed (r01_r01_to_r01' (r1,r2))"
using biexp01_well_formed_comb[of "r01_binary_expansion' (fst (r1,r2))" "r01_binary_expansion' (snd (r1,r2))"] r01_binary_expansion_well_formed[of r1] r01_binary_expansion_well_formed[of r2] assms
by (auto simp add: r01_r01_to_r01'_def)
definition r01_r01_to_r01_sum :: "real à real â nat â real" where
"r01_r01_to_r01_sum â¡ r01_binary_sum â r01_r01_to_r01'"
definition r01_r01_to_r01 :: "real à real â real" where
"r01_r01_to_r01 â¡ lim â r01_r01_to_r01_sum"
lemma r01_r01_to_r01_def':
"r01_r01_to_r01 (r1,r2) = (ân. real (r01_r01_to_r01' (r1,r2) n) * (1/2)^(n+1))"
proof -
have "r01_r01_to_r01_sum (r1,r2) = (λn. (âi = 0..n. real (r01_r01_to_r01' (r1,r2) i) * (1 / 2) ^ Suc i))"
by(auto simp add: r01_r01_to_r01_sum_def r01_binary_sum_def)
thus ?thesis
using lim_sum_ai[of "λn. r01_r01_to_r01' (r1,r2) n"] r01_r01_to_r01'in01
by(simp add: r01_r01_to_r01_def)
qed
lemma r01_r01_to_r01_measurable:
"r01_r01_to_r01 â real_borel â¨â©M real_borel ââ©M real_borel"
proof -
have "r01_r01_to_r01 = (λx. ân. real (r01_r01_to_r01' x n) * (1/2)^(n+1))"
using r01_r01_to_r01_def' by auto
also have "... â real_borel â¨â©M real_borel ââ©M real_borel"
proof(rule borel_measurable_suminf)
fix n :: nat
have "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) = (λr. r * (1/2)^(n+1)) â (λx. real (r01_r01_to_r01' x n))"
by auto
also have "... â borel_measurable (borel â¨â©M borel)"
proof(rule measurable_comp[of _ _ borel])
have "(λx. real (r01_r01_to_r01' x n))
= (λx. if even n then real (r01_binary_expansion' (fst x) (n div 2)) else real (r01_binary_expansion' (snd x) ((n - 1) div 2)))"
by (auto simp add: r01_r01_to_r01'_def)
also have "... â borel_measurable (borel â¨â©M borel)"
using r01_binary_expansion'_measurable by simp
finally show "(λx. real (r01_r01_to_r01' x n)) â borel_measurable (borel â¨â©M borel)" .
next
show "(λr::real. r * (1 / 2) ^ (n + 1)) â borel_measurable borel"
by simp
qed
finally show "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) â borel_measurable (borel â¨â©M borel)" .
qed
finally show ?thesis .
qed
lemma r01_r01_to_r01_image:
assumes "0 < r1" "r1 < 1"
shows "r01_r01_to_r01 (r1,r2) â {0<..<1}"
proof -
obtain i where "r01_binary_expansion' r1 i = 1"
using r01_binary_expression_ex1[of r1] assms(1,2)
by auto
hence hi:"r01_r01_to_r01' (r1,r2) (2*i) = 1"
by(simp add: r01_r01_to_r01'_def)
obtain j where "r01_binary_expansion' r1 j = 0"
using r01_binary_expression_ex0[of r1] assms(1,2)
by auto
hence hj:"r01_r01_to_r01' (r1,r2) (2*j) = 0"
by(simp add: r01_r01_to_r01'_def)
show ?thesis
using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj
by auto
qed
lemma r01_r01_to_r01_image':
assumes "0 < r2" "r2 < 1"
shows "r01_r01_to_r01 (r1,r2) â {0<..<1}"
proof -
obtain i where "r01_binary_expansion' r2 i = 1"
using r01_binary_expression_ex1[of r2] assms(1,2)
by auto
hence hi:"r01_r01_to_r01' (r1,r2) (2*i + 1) = 1"
by(simp add: r01_r01_to_r01'_def)
obtain j where "r01_binary_expansion' r2 j = 0"
using r01_binary_expression_ex0[of r2] assms(1,2)
by auto
hence hj:"r01_r01_to_r01' (r1,r2) (2*j + 1) = 0"
by(simp add: r01_r01_to_r01'_def)
show ?thesis
using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj
by auto
qed
lemma r01_r01_to_r01_binary_nth:
assumes "0 < r1" "r1 < 1"
and "0 < r2" "r2 < 1"
shows "r01_binary_expansion' r1 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n) â§
r01_binary_expansion' r2 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n + 1)"
proof -
have "ân. r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) n = r01_r01_to_r01' (r1,r2) n"
using r01_r01_to_r01_def'[of r1 r2] biexp01_well_formed_an[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'_well_formed[of r1 r2] assms
by simp
thus ?thesis
by(simp add: r01_r01_to_r01'_def)
qed
lemma r01_r01__r01__r01_r01_id:
assumes "0 < r1" "r1 < 1"
"0 < r2" "r2 < 1"
shows "(r01_to_r01_r01 â r01_r01_to_r01) (r1,r2) = (r1,r2)"
proof
show "fst ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = fst (r1, r2)"
proof -
have "fst ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_fst (r01_r01_to_r01 (r1,r2))"
by(simp add: r01_to_r01_r01_def)
also have "... = (ân. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n)) * (1 / 2) ^ (n + 1))"
using r01_to_r01_r01_fst_def'[of "r01_r01_to_r01 (r1,r2)"] by simp
also have "... = (ân. real (r01_binary_expansion' r1 n) * (1 / 2) ^ (n + 1))"
using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp
also have "... = r1"
using r01_binary_expression_correct[of r1] assms(1,2)
by simp
finally show ?thesis by simp
qed
next
show "snd ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = snd (r1, r2)"
proof -
have "snd ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_snd (r01_r01_to_r01 (r1,r2))"
by(simp add: r01_to_r01_r01_def)
also have "... = (ân. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n + 1)) * (1 / 2) ^ (n + 1))"
using r01_to_r01_r01_snd_def'[of "r01_r01_to_r01 (r1,r2)"] by simp
also have "... = (ân. real (r01_binary_expansion' r2 n) * (1 / 2) ^ (n + 1))"
using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp
also have "... = r2"
using r01_binary_expression_correct[of r2] assms(3,4)
by simp
finally show ?thesis by simp
qed
qed
text â¹ We first show that â¹M â¨â©M N⺠is a standard Borel space for standard Borel spaces â¹M⺠and â¹Nâº.âº
lemma pair_measurable[measurable]:
assumes "f â X ââ©M Y"
and "g â X' ââ©M Y'"
shows "map_prod f g â X â¨â©M X' ââ©M Y â¨â©M Y'"
using assms by(auto simp add: measurable_pair_iff)
lemma pair_standard_borel_standard:
assumes "standard_borel M"
and "standard_borel N"
shows "standard_borel (M â¨â©M N)"
proof -
define rr_to_r :: "real à real â real"
where "rr_to_r â¡ real_to_01open_inverse â r01_r01_to_r01 â (λ(x,y). (real_to_01open x, real_to_01open y))"
have 1[measurable]: "rr_to_r â real_borel â¨â©M real_borel ââ©M real_borel"
proof -
have "(λ(x,y). (real_to_01open x, real_to_01open y)) â real_borel â¨â©M real_borel ââ©M real_borel â¨â©M real_borel"
using borel_measurable_continuous_onI[OF real_to_01open_continuous]
by simp
from measurable_restrict_space2[OF _ this,of "{0<..<1}Ã{0<..<1}"]
have [measurable]:"(λ(x,y). (real_to_01open x, real_to_01open y)) â real_borel â¨â©M real_borel ââ©M restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1})"
by(simp add: split_beta' real_to_01open_01)
have [measurable]: "r01_r01_to_r01 â restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1}) ââ©M restrict_space real_borel {0<..<1}"
using r01_r01_to_r01_image' by(auto intro!: measurable_restrict_space3[OF r01_r01_to_r01_measurable])
thus ?thesis
using borel_measurable_continuous_on_restrict[OF real_to_01open_inverse_continuous]
by(simp add: rr_to_r_def)
qed
define r_to_01 :: "real â real"
where "r_to_01 â¡ (λr. if r â real_to_01open -` (r01_to_r01_r01 -` ({0<..<1}Ã{0<..<1})) then real_to_01open r else 3/4)"
define r01_to_r01_r01' :: "real â real à real"
where "r01_to_r01_r01' â¡ (λr. if r â r01_to_r01_r01 -` ({0<..<1}Ã{0<..<1}) then r01_to_r01_r01 r else (1/2,1/2))"
define r_to_rr :: "real â real à real"
where "r_to_rr â¡ (λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) â r01_to_r01_r01' â r_to_01"
have 2[measurable]: "r_to_rr â real_borel ââ©M real_borel â¨â©M real_borel"
proof -
have 1: "{0<..<1}Ã{0<..<1} â sets (restrict_space (real_borel â¨â©M real_borel) ({0..1}Ã{0..1}))"
by(auto simp: sets_restrict_space_iff)
have 2[measurable]: "real_to_01open â real_borel ââ©M restrict_space real_borel {0<..<1}"
using measurable_restrict_space2[OF _ borel_measurable_continuous_onI[OF real_to_01open_continuous] ,of "{0<..<1}"]
by(simp add: real_to_01open_01)
have 3: "real_to_01open -` space (restrict_space real_borel {0<..<1}) = UNIV"
using real_to_01open_01 by auto
have "r01_to_r01_r01 â restrict_space real_borel {0<..<1} ââ©M restrict_space (real_borel â¨â©M real_borel) ({0..1}Ã{0..1})"
using r01_to_r01_r01_image measurable_restrict_space3[OF r01_to_r01_r01_measurable] by simp
note 4 = measurable_sets[OF this 1]
note 5 = measurable_sets[OF 2 4,simplified vimage_Int 3,simplified]
have [measurable]:"r_to_01 â real_borel ââ©M restrict_space real_borel {0<..<1}"
unfolding r_to_01_def
by(rule measurable_If_set) (auto intro!: measurable_restrict_space2 simp: 5)
have [measurable]: "r01_to_r01_r01' â restrict_space real_borel {0<..<1} ââ©M restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1})"
using 4 r01_to_r01_r01_measurable
by(auto intro!: measurable_restrict_space3 simp: r01_to_r01_r01'_def)
have [measurable]: "(λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) â restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1}) ââ©M real_borel â¨â©M real_borel"
using borel_measurable_continuous_on_restrict[OF continuous_on_Pair[OF continuous_on_compose[of "{0<..<1::real}Ã{0<..<1::real}",OF continuous_on_fst[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous] continuous_on_compose[of "{0<..<1::real}Ã{0<..<1::real}",OF continuous_on_snd[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous]]]
by(simp add: split_beta' borel_prod)
show ?thesis
by(simp add: r_to_rr_def)
qed
have 3: "âx. r_to_rr (rr_to_r x) = x"
using r01_to_r01_r01_image r01_r01_to_r01_image r01_r01__r01__r01_r01_id real_to_01open_01 real_to_01open_inverse_correct' fun_cong[OF real_to_01open_inverse_correct]
by(auto simp add: r01_to_r01_r01'_def r_to_01_def comp_def split_beta' r_to_rr_def rr_to_r_def)
interpret s1: standard_borel M by fact
interpret s2: standard_borel N by fact
show ?thesis
by(auto intro!: standard_borelI[where f="rr_to_r â map_prod s1.f s2.f" and g="map_prod s1.g s2.g â r_to_rr"] simp: 3 space_pair_measure)
qed
lemma pair_standard_borel_spaceUNIV:
assumes "standard_borel_space_UNIV M"
and "standard_borel_space_UNIV N"
shows "standard_borel_space_UNIV (M â¨â©M N)"
apply(rule standard_borel_space_UNIVI')
using assms pair_standard_borel_standard[of M N]
by(auto simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def space_pair_measure)
locale pair_standard_borel = s1: standard_borel M + s2: standard_borel N
for M :: "'a measure" and N :: "'b measure"
begin
sublocale standard_borel "M â¨â©M N"
by(auto intro!: pair_standard_borel_standard)
end
locale pair_standard_borel_space_UNIV = s1: standard_borel_space_UNIV M + s2: standard_borel_space_UNIV N
for M :: "'a measure" and N :: "'b measure"
begin
sublocale pair_standard_borel M N
by standard
sublocale standard_borel_space_UNIV "M â¨â©M N"
by(auto intro!: pair_standard_borel_spaceUNIV
simp: s1.standard_borel_space_UNIV_axioms s2.standard_borel_space_UNIV_axioms)
end
text â¹$\mathbb{R}\times\mathbb{R}$ is a standard Borel space.âº
interpretation real_real : pair_standard_borel_space_UNIV real_borel real_borel
by(auto intro!: pair_standard_borel_spaceUNIV simp: real.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def)
subsection â¹ $\mathbb{N}\times\mathbb{R}$ âº
text â¹ $\mathbb{N}\times\mathbb{R}$ is a standard Borel space. âº
interpretation nat_real: pair_standard_borel_space_UNIV nat_borel real_borel
by(auto intro!: pair_standard_borel_spaceUNIV
simp: real.standard_borel_space_UNIV_axioms nat.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def)
end>
Theory QuasiBorel
section â¹Quasi-Borel Spacesâº
theory QuasiBorel
imports "StandardBorel"
begin
subsection â¹ Definitions âº
text â¹ We formalize quasi-Borel spaces introduced by Heunen et al.~\cite{Heunen_2017}.âº
subsubsection â¹ Quasi-Borel Spacesâº
definition qbs_closed1 :: "(real â 'a) set â bool"
where "qbs_closed1 Mx â¡ (âa â Mx. âf â real_borel ââ©M real_borel. a â f â Mx)"
definition qbs_closed2 :: "['a set, (real â 'a) set] â bool"
where "qbs_closed2 X Mx â¡ (âx â X. (λr. x) â Mx)"
definition qbs_closed3 :: "(real â 'a) set â bool"
where "qbs_closed3 Mx â¡ (âP::real â nat. âFi::nat â real â 'a.
(âi. P -` {i} â sets real_borel)
â¶ (âi. Fi i â Mx)
â¶ (λr. Fi (P r) r) â Mx)"
lemma separate_measurable:
fixes P :: "real â nat"
assumes "âi. P -` {i} â sets real_borel"
shows "P â real_borel ââ©M nat_borel"
proof -
have "P â real_borel ââ©M count_space UNIV"
by (auto simp add: assms measurable_count_space_eq_countable)
thus ?thesis
using measurable_cong_sets sets_borel_eq_count_space by blast
qed
lemma measurable_separate:
fixes P :: "real â nat"
assumes "P â real_borel ââ©M nat_borel"
shows "P -` {i} â sets real_borel"
by(rule measurable_sets_borel[OF assms borel_singleton[OF sets.empty_sets,of i]])
definition "is_quasi_borel X Mx â· Mx â UNIV â X â§ qbs_closed1 Mx â§ qbs_closed2 X Mx â§ qbs_closed3 Mx"
lemma is_quasi_borel_intro[simp]:
assumes "Mx â UNIV â X"
and "qbs_closed1 Mx" "qbs_closed2 X Mx" "qbs_closed3 Mx"
shows "is_quasi_borel X Mx"
using assms by(simp add: is_quasi_borel_def)
typedef 'a quasi_borel = "{(X::'a set, Mx). is_quasi_borel X Mx}"
proof
show "(UNIV, UNIV) â {(X::'a set, Mx). is_quasi_borel X Mx}"
by (simp add: is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)
qed
definition qbs_space :: "'a quasi_borel â 'a set" where
"qbs_space X â¡ fst (Rep_quasi_borel X)"
definition qbs_Mx :: "'a quasi_borel â (real â 'a) set" where
"qbs_Mx X â¡ snd (Rep_quasi_borel X)"
lemma qbs_decomp :
"(qbs_space X,qbs_Mx X) â {(X::'a set, Mx). is_quasi_borel X Mx}"
by (simp add: qbs_space_def qbs_Mx_def Rep_quasi_borel[simplified])
lemma qbs_Mx_to_X[dest]:
assumes "α â qbs_Mx X"
shows "α â UNIV â qbs_space X"
"α r â qbs_space X"
using qbs_decomp assms by(auto simp: is_quasi_borel_def)
lemma qbs_closed1I:
assumes "âα f. α â Mx â¹ f â real_borel ââ©M real_borel ⹠α â f â Mx"
shows "qbs_closed1 Mx"
using assms by(simp add: qbs_closed1_def)
lemma qbs_closed1_dest[simp]:
assumes "α â qbs_Mx X"
and "f â real_borel ââ©M real_borel"
shows "α â f â qbs_Mx X"
using assms qbs_decomp by (auto simp add: is_quasi_borel_def qbs_closed1_def)
lemma qbs_closed2I:
assumes "âx. x â X â¹ (λr. x) â Mx"
shows "qbs_closed2 X Mx"
using assms by(simp add: qbs_closed2_def)
lemma qbs_closed2_dest[simp]:
assumes "x â qbs_space X"
shows "(λr. x) â qbs_Mx X"
using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed2_def)
lemma qbs_closed3I:
assumes "â(P :: real â nat) Fi. (âi. P -` {i} â sets real_borel) â¹ (âi. Fi i â Mx)
â¹ (λr. Fi (P r) r) â Mx"
shows "qbs_closed3 Mx"
using assms by(auto simp: qbs_closed3_def)
lemma qbs_closed3I':
assumes "â(P :: real â nat) Fi. P â real_borel ââ©M nat_borel â¹ (âi. Fi i â Mx)
â¹ (λr. Fi (P r) r) â Mx"
shows "qbs_closed3 Mx"
using assms by(auto intro!: qbs_closed3I simp: separate_measurable)
lemma qbs_closed3_dest[simp]:
fixes P::"real â nat" and Fi :: "nat â real â _"
assumes "âi. P -` {i} â sets real_borel"
and "âi. Fi i â qbs_Mx X"
shows "(λr. Fi (P r) r) â qbs_Mx X"
using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed3_def)
lemma qbs_closed3_dest':
fixes P::"real â nat" and Fi :: "nat â real â _"
assumes "P â real_borel ââ©M nat_borel"
and "âi. Fi i â qbs_Mx X"
shows "(λr. Fi (P r) r) â qbs_Mx X"
using qbs_closed3_dest[OF measurable_separate[OF assms(1)] assms(2)] .
lemma qbs_closed3_dest2:
assumes "countable I"
and [measurable]: "P â real_borel ââ©M count_space I"
and "âi. i â I â¹ Fi i â qbs_Mx X"
shows "(λr. Fi (P r) r) â qbs_Mx X"
proof -
have 0:"I â {}"
using measurable_empty_iff[of "count_space I" P real_borel] assms(2)
by fastforce
define P' where "P' â¡ to_nat_on I â P"
define Fi' where "Fi' â¡ Fi â (from_nat_into I)"
have 1:"P' â real_borel ââ©M nat_borel"
by(simp add: P'_def)
have 2:"âi. Fi' i â qbs_Mx X"
using assms(3) from_nat_into[OF 0] by(simp add: Fi'_def)
have "(λr. Fi' (P' r) r) â qbs_Mx X"
using 1 2 measurable_separate by auto
thus ?thesis
using from_nat_into_to_nat_on[OF assms(1)] measurable_space[OF assms(2)]
by(auto simp: Fi'_def P'_def)
qed
lemma qbs_closed3_dest2':
assumes "countable I"
and [measurable]: "P â real_borel ââ©M count_space I"
and "âi. i â range P â¹ Fi i â qbs_Mx X"
shows "(λr. Fi (P r) r) â qbs_Mx X"
proof -
have 0:"range P â© I = range P"
using measurable_space[OF assms(2)] by auto
have 1:"P â real_borel ââ©M count_space (range P)"
using restrict_count_space[of I "range P"] measurable_restrict_space2[OF _ assms(2),of "range P"]
by(simp add: 0)
have 2:"countable (range P)"
using countable_Int2[OF assms(1),of "range P"]
by(simp add: 0)
show ?thesis
by(auto intro!: qbs_closed3_dest2[OF 2 1 assms(3)])
qed
lemma qbs_space_Mx:
"qbs_space X = {α x |x α. α â qbs_Mx X}"
proof auto
fix x
assume 1:"x â qbs_space X"
show "âxa α. x = α xa ⧠α â qbs_Mx X"
by(auto intro!: exI[where x=0] exI[where x="(λr. x)"] simp: 1)
qed
lemma qbs_space_eq_Mx:
assumes "qbs_Mx X = qbs_Mx Y"
shows "qbs_space X = qbs_space Y"
by(simp add: qbs_space_Mx assms)
lemma qbs_eqI:
assumes "qbs_Mx X = qbs_Mx Y"
shows "X = Y"
by (metis Rep_quasi_borel_inverse prod.exhaust_sel qbs_Mx_def qbs_space_def assms qbs_space_eq_Mx[OF assms])
subsubsection â¹ Morphism of Quasi-Borel Spaces âº
definition qbs_morphism :: "['a quasi_borel, 'b quasi_borel] â ('a â 'b) set" (infixr "ââ©Q" 60) where
"X ââ©Q Y â¡ {f â qbs_space X â qbs_space Y. âα â qbs_Mx X. f â α â qbs_Mx Y}"
lemma qbs_morphismI:
assumes "âα. α â qbs_Mx X â¹ f â α â qbs_Mx Y"
shows "f â X ââ©Q Y"
proof -
have "f â qbs_space X â qbs_space Y"
proof
fix x
assume "x â qbs_space X "
then have "(λr. x) â qbs_Mx X"
by simp
hence "f â (λr. x) â qbs_Mx Y"
using assms by blast
thus "f x â qbs_space Y"
by auto
qed
thus ?thesis
using assms by(simp add: qbs_morphism_def)
qed
lemma qbs_morphismE[dest]:
assumes "f â X ââ©Q Y"
shows "f â qbs_space X â qbs_space Y"
"âx. x â qbs_space X â¹ f x â qbs_space Y"
"âα. α â qbs_Mx X â¹ f â α â qbs_Mx Y"
using assms by(auto simp add: qbs_morphism_def)
lemma qbs_morphism_ident[simp]:
"id â X ââ©Q X"
by(auto intro: qbs_morphismI)
lemma qbs_morphism_ident'[simp]:
"(λx. x) â X ââ©Q X"
using qbs_morphism_ident by(simp add: id_def)
lemma qbs_morphism_comp:
assumes "f â X ââ©Q Y" "g â Y ââ©Q Z"
shows "g â f â X ââ©Q Z"
using assms by (simp add: comp_assoc Pi_def qbs_morphism_def)
lemma qbs_morphism_cong:
assumes "âx. x â qbs_space X â¹ f x = g x"
and "f â X ââ©Q Y"
shows "g â X ââ©Q Y"
proof(rule qbs_morphismI)
fix α
assume 1:"α â qbs_Mx X"
have "g â α = f â α"
proof
fix x
have "α x â qbs_space X"
using 1 qbs_decomp[of X] by auto
thus "(g â α) x = (f â α) x"
using assms(1) by simp
qed
thus "g â α â qbs_Mx Y"
using 1 assms(2) by(simp add: qbs_morphism_def)
qed
lemma qbs_morphism_const:
assumes "y â qbs_space Y"
shows "(λ_. y) â X ââ©Q Y"
using assms by (auto intro: qbs_morphismI)
subsubsection â¹ Empty Space âº
definition empty_quasi_borel :: "'a quasi_borel" where
"empty_quasi_borel â¡ Abs_quasi_borel ({},{})"
lemma eqb_correct: "Rep_quasi_borel empty_quasi_borel = ({}, {})"
using Abs_quasi_borel_inverse
by(auto simp add: Abs_quasi_borel_inverse empty_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
lemma eqb_space[simp]: "qbs_space empty_quasi_borel = {}"
by(simp add: qbs_space_def eqb_correct)
lemma eqb_Mx[simp]: "qbs_Mx empty_quasi_borel = {}"
by(simp add: qbs_Mx_def eqb_correct)
lemma qbs_empty_equiv :"qbs_space X = {} â· qbs_Mx X = {}"
proof(auto)
fix x
assume "qbs_Mx X = {}"
and h:"x â qbs_space X"
have "(λr. x) â qbs_Mx X"
using h by simp
thus "False" using â¹qbs_Mx X = {}⺠by simp
qed
lemma empty_quasi_borel_iff:
"qbs_space X = {} â· X = empty_quasi_borel"
by(auto intro!: qbs_eqI)
subsubsection â¹ Unit Space âº
definition unit_quasi_borel :: "unit quasi_borel" ("1â©Q") where
"unit_quasi_borel â¡ Abs_quasi_borel (UNIV,UNIV)"
lemma uqb_correct: "Rep_quasi_borel unit_quasi_borel = (UNIV,UNIV)"
using Abs_quasi_borel_inverse
by(auto simp add: unit_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
lemma uqb_space[simp]: "qbs_space unit_quasi_borel = {()}"
by(simp add: qbs_space_def UNIV_unit uqb_correct)
lemma uqb_Mx[simp]: "qbs_Mx unit_quasi_borel = {λr. ()}"
by(auto simp add: qbs_Mx_def uqb_correct)
lemma unit_quasi_borel_terminal:
"â! f. f â X ââ©Q unit_quasi_borel"
by(fastforce simp: qbs_morphism_def)
definition to_unit_quasi_borel :: "'a â unit" ("!â©Q") where
"to_unit_quasi_borel ⡠(λ_.())"
lemma to_unit_quasi_borel_morphism :
"!â©Q â X ââ©Q unit_quasi_borel"
by(auto simp add: to_unit_quasi_borel_def qbs_morphism_def)
subsubsection â¹ Subspaces âº
definition sub_qbs :: "['a quasi_borel, 'a set] â 'a quasi_borel" where
"sub_qbs X U â¡ Abs_quasi_borel (qbs_space X â© U,{f â UNIV â qbs_space X â© U. f â qbs_Mx X})"
lemma sub_qbs_closed:
"qbs_closed1 {f â UNIV â qbs_space X â© U. f â qbs_Mx X}"
"qbs_closed2 (qbs_space X â© U) {f â UNIV â qbs_space X â© U. f â qbs_Mx X}"
"qbs_closed3 {f â UNIV â qbs_space X â© U. f â qbs_Mx X}"
unfolding qbs_closed1_def qbs_closed2_def qbs_closed3_def by auto
lemma sub_qbs_correct[simp]: "Rep_quasi_borel (sub_qbs X U) = (qbs_space X â© U,{f â UNIV â qbs_space X â© U. f â qbs_Mx X})"
by(simp add: Abs_quasi_borel_inverse sub_qbs_def sub_qbs_closed)
lemma sub_qbs_space[simp]: "qbs_space (sub_qbs X U) = qbs_space X â© U"
by(simp add: qbs_space_def)
lemma sub_qbs_Mx[simp]: "qbs_Mx (sub_qbs X U) = {f â UNIV â qbs_space X â© U. f â qbs_Mx X}"
by(simp add: qbs_Mx_def)
lemma sub_qbs:
assumes "U â qbs_space X"
shows "(qbs_space (sub_qbs X U), qbs_Mx (sub_qbs X U)) = (U, {f â UNIV â U. f â qbs_Mx X})"
using assms by auto
subsubsection â¹ Image Spaces âº
definition map_qbs :: "['a â 'b] â 'a quasi_borel â 'b quasi_borel" where
"map_qbs f X = Abs_quasi_borel (f ` (qbs_space X),{β. âαâ qbs_Mx X. β = f â α})"
lemma map_qbs_f:
"{β. âαâ qbs_Mx X. β = f â α} â UNIV â f ` (qbs_space X)"
by fastforce
lemma map_qbs_closed1:
"qbs_closed1 {β. âαâ qbs_Mx X. β = f â α}"
unfolding qbs_closed1_def
using qbs_closed1_dest by(fastforce simp: comp_def)
lemma map_qbs_closed2:
"qbs_closed2 (f ` (qbs_space X)) {β. âαâ qbs_Mx X. β = f â α}"
unfolding qbs_closed2_def by fastforce
lemma map_qbs_closed3:
"qbs_closed3 {β. âαâ qbs_Mx X. β = f â α}"
proof(auto simp add: qbs_closed3_def)
fix P Fi
assume h:"âi::nat. P -` {i} â sets real_borel"
"âi::nat. âαâqbs_Mx X. Fi i = f â α"
then obtain αi
where ha: "âi::nat. αi i â qbs_Mx X â§ Fi i = f â (αi i)"
by metis
hence 1:"(λr. αi (P r) r) â qbs_Mx X"
using h(1) by fastforce
show "âαâqbs_Mx X. (λr. Fi (P r) r) = f â α"
by(auto intro!: bexI[where x="(λr. αi (P r) r)"] simp add: 1 ha comp_def)
qed
lemma map_qbs_correct[simp]:
"Rep_quasi_borel (map_qbs f X) = (f ` (qbs_space X),{β. âαâ qbs_Mx X. β = f â α})"
unfolding map_qbs_def
by(simp add: Abs_quasi_borel_inverse map_qbs_f map_qbs_closed1 map_qbs_closed2 map_qbs_closed3)
lemma map_qbs_space[simp]:
"qbs_space (map_qbs f X) = f ` (qbs_space X)"
by(simp add: qbs_space_def)
lemma map_qbs_Mx[simp]:
"qbs_Mx (map_qbs f X) = {β. âαâ qbs_Mx X. β = f â α}"
by(simp add: qbs_Mx_def)
inductive_set generating_Mx :: "'a set â (real â 'a) set â (real â 'a) set"
for X :: "'a set" and Mx :: "(real â 'a) set"
where
Basic: "α â Mx ⹠α â generating_Mx X Mx"
| Const: "x â X â¹ (λr. x) â generating_Mx X Mx"
| Comp : "f â real_borel ââ©M real_borel ⹠α â generating_Mx X Mx ⹠α â f â generating_Mx X Mx"
| Part : "(âi. Fi i â generating_Mx X Mx) â¹ P â real_borel ââ©M nat_borel â¹ (λr. Fi (P r) r) â generating_Mx X Mx"
lemma generating_Mx_to_space:
assumes "Mx â UNIV â X"
shows "generating_Mx X Mx â UNIV â X"
proof
fix α
assume "α â generating_Mx X Mx"
then show "α â UNIV â X"
by(induct rule: generating_Mx.induct) (use assms in auto)
qed
lemma generating_Mx_closed1:
"qbs_closed1 (generating_Mx X Mx)"
by (simp add: generating_Mx.Comp qbs_closed1I)
lemma generating_Mx_closed2:
"qbs_closed2 X (generating_Mx X Mx)"
by (simp add: generating_Mx.Const qbs_closed2I)
lemma generating_Mx_closed3:
"qbs_closed3 (generating_Mx X Mx)"
by(simp add: qbs_closed3I' generating_Mx.Part)
lemma generating_Mx_Mx:
"generating_Mx (qbs_space X) (qbs_Mx X) = qbs_Mx X"
proof auto
fix α
assume "α â generating_Mx (qbs_space X) (qbs_Mx X)"
then show "α â qbs_Mx X"
by(rule generating_Mx.induct) (auto intro!: qbs_closed1_dest[simplified comp_def] simp: qbs_closed3_dest')
next
fix α
assume "α â qbs_Mx X"
then show "α â generating_Mx (qbs_space X) (qbs_Mx X)" ..
qed
subsubsection â¹ Ordering of Quasi-Borel Spaces âº
instantiation quasi_borel :: (type) order_bot
begin
inductive less_eq_quasi_borel :: "'a quasi_borel â 'a quasi_borel â bool" where
"qbs_space X â qbs_space Y â¹ less_eq_quasi_borel X Y"
| "qbs_space X = qbs_space Y â¹ qbs_Mx Y â qbs_Mx X â¹ less_eq_quasi_borel X Y"
lemma le_quasi_borel_iff:
"X ⤠Y â· (if qbs_space X = qbs_space Y then qbs_Mx Y â qbs_Mx X else qbs_space X â qbs_space Y)"
by(auto elim: less_eq_quasi_borel.cases intro: less_eq_quasi_borel.intros)
definition less_quasi_borel :: "'a quasi_borel â 'a quasi_borel â bool" where
"less_quasi_borel X Y ⷠ(X ⤠Y ⧠¬ Y ⤠X)"
definition bot_quasi_borel :: "'a quasi_borel" where
"bot_quasi_borel = empty_quasi_borel"
instance
proof
show "bot ⤠a" for a :: "'a quasi_borel"
using qbs_empty_equiv
by(auto simp add: le_quasi_borel_iff bot_quasi_borel_def)
qed (auto simp: le_quasi_borel_iff less_quasi_borel_def split: if_split_asm intro: qbs_eqI)
end
definition inf_quasi_borel :: "['a quasi_borel, 'a quasi_borel] â 'a quasi_borel" where
"inf_quasi_borel X X' = Abs_quasi_borel (qbs_space X â© qbs_space X', qbs_Mx X â© qbs_Mx X')"
lemma inf_quasi_borel_correct: "Rep_quasi_borel (inf_quasi_borel X X') = (qbs_space X â© qbs_space X', qbs_Mx X â© qbs_Mx X')"
by(fastforce intro!: Abs_quasi_borel_inverse
simp: inf_quasi_borel_def is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)
lemma inf_qbs_space[simp]: "qbs_space (inf_quasi_borel X X') = qbs_space X â© qbs_space X'"
by (simp add: qbs_space_def inf_quasi_borel_correct)
lemma inf_qbs_Mx[simp]: "qbs_Mx (inf_quasi_borel X X') = qbs_Mx X â© qbs_Mx X'"
by(simp add: qbs_Mx_def inf_quasi_borel_correct)
definition max_quasi_borel :: "'a set â 'a quasi_borel" where
"max_quasi_borel X = Abs_quasi_borel (X, UNIV â X)"
lemma max_quasi_borel_correct: "Rep_quasi_borel (max_quasi_borel X) = (X, UNIV â X)"
by(fastforce intro!: Abs_quasi_borel_inverse
simp: max_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
lemma max_qbs_space[simp]: "qbs_space (max_quasi_borel X) = X"
by(simp add: qbs_space_def max_quasi_borel_correct)
lemma max_qbs_Mx[simp]: "qbs_Mx (max_quasi_borel X) = UNIV â X"
by(simp add: qbs_Mx_def max_quasi_borel_correct)
instantiation quasi_borel :: (type) semilattice_sup
begin
definition sup_quasi_borel :: "'a quasi_borel â 'a quasi_borel â 'a quasi_borel" where
"sup_quasi_borel X Y â¡ (if qbs_space X = qbs_space Y then inf_quasi_borel X Y
else if qbs_space X â qbs_space Y then Y
else if qbs_space Y â qbs_space X then X
else max_quasi_borel (qbs_space X ⪠qbs_space Y))"
instance
proof
fix X Y :: "'a quasi_borel"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
consider "?X = ?Y" | "?X â ?Y" | "?Y â ?X" | "?X â ?X ⪠?Y â§ ?Y â ?X ⪠?Y"
by auto
then show "X ⤠X â Y"
proof(cases)
case 1
show ?thesis
unfolding sup_quasi_borel_def
by(rule less_eq_quasi_borel.intros(2),simp_all add: 1)
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
by (simp add: less_eq_quasi_borel.intros(1))
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
by auto
next
case 4
then show ?thesis
unfolding sup_quasi_borel_def
by(auto simp: less_eq_quasi_borel.intros(1))
qed
next
fix X Y :: "'a quasi_borel"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
consider "?X = ?Y" | "?X â ?Y" | "?Y â ?X" | "?X â ?X ⪠?Y â§ ?Y â ?X ⪠?Y"
by auto
then show "Y ⤠X â Y"
proof(cases)
case 1
show ?thesis
unfolding sup_quasi_borel_def
by(rule less_eq_quasi_borel.intros(2)) (simp_all add: 1)
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
by auto
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
by (auto simp add: less_eq_quasi_borel.intros(1))
next
case 4
then show ?thesis
unfolding sup_quasi_borel_def
by(auto simp: less_eq_quasi_borel.intros(1))
qed
next
fix X Y Z :: "'a quasi_borel"
assume h:"X ⤠Z" "Y ⤠Z"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
let ?Z = "qbs_space Z"
consider "?X = ?Y" | "?X â ?Y" | "?Y â ?X" | "?X â ?X ⪠?Y â§ ?Y â ?X ⪠?Y"
by auto
then show "sup X Y ⤠Z"
proof cases
case 1
show ?thesis
unfolding sup_quasi_borel_def
apply(simp add: 1,rule less_eq_quasi_borel.cases[OF h(1)])
apply(rule less_eq_quasi_borel.intros(1))
apply auto[1]
apply auto
apply(rule less_eq_quasi_borel.intros(2))
apply(simp add: 1)
by(rule less_eq_quasi_borel.cases[OF h(2)]) (auto simp: 1)
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
using h(2) by auto
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
using h(1) by auto
next
case 4
then have [simp]:"?X â ?Y" "~ (?X â ?Y)" "~ (?Y â ?X)"
by auto
have [simp]:"?X â ?Z" "?Y â ?Z"
by (metis h(1) dual_order.order_iff_strict less_eq_quasi_borel.cases)
(metis h(2) dual_order.order_iff_strict less_eq_quasi_borel.cases)
then consider "?X ⪠?Y = ?Z" | "?X ⪠?Y â ?Z"
by blast
then show ?thesis
unfolding sup_quasi_borel_def
apply cases
apply simp
apply(rule less_eq_quasi_borel.intros(2))
apply simp
apply auto[1]
by(simp add: less_eq_quasi_borel.intros(1))
qed
qed
end
endle>
Theory Measure_QuasiBorel_Adjunction
subsection â¹Relation to Measurable Spacesâº
theory Measure_QuasiBorel_Adjunction
imports "QuasiBorel"
begin
text â¹ We construct the adjunction between \textbf{Meas} and \textbf{QBS},
where \textbf{Meas} is the category of measurable spaces and measurable functions
and \textbf{QBS} is the category of quasi-Borel spaces and morphisms.âº
subsubsection â¹ The Functor $R$ âº
definition measure_to_qbs :: "'a measure â 'a quasi_borel" where
"measure_to_qbs X â¡ Abs_quasi_borel (space X, real_borel ââ©M X)"
lemma R_Mx_correct: "real_borel ââ©M X â UNIV â space X"
by (simp add: measurable_space subsetI)
lemma R_qbs_closed1: "qbs_closed1 (real_borel ââ©M X)"
by (simp add: qbs_closed1_def)
lemma R_qbs_closed2: "qbs_closed2 (space X) (real_borel ââ©M X)"
by (simp add: qbs_closed2_def)
lemma R_qbs_closed3: "qbs_closed3 (real_borel ââ©M (X :: 'a measure))"
proof(rule qbs_closed3I)
fix P::"real â nat"
fix Fi::"nat â real â 'a"
assume h:"âi. P -` {i} â sets real_borel"
"âi. Fi i â real_borel ââ©M X"
show "(λr. Fi (P r) r) â real_borel ââ©M X"
proof(rule measurableI)
fix x
assume "x â space real_borel"
then show "Fi (P x) x â space X"
using h(2) measurable_space[of "Fi (P x)" real_borel X x]
by auto
next
fix A
assume h':"A â sets X"
have "(λr. Fi (P r) r) -` A = (âi::nat. ((Fi i -` A) â© (P -` {i})))"
by auto
also have "... â sets real_borel"
using sets.Int measurable_sets[OF h(2) h'] h(1)
by(auto intro!: countable_Un_Int(1))
finally show "(λr. Fi (P r) r) -` A â© space real_borel â sets real_borel"
by simp
qed
qed
lemma R_correct[simp]: "Rep_quasi_borel (measure_to_qbs X) = (space X, real_borel ââ©M X)"
unfolding measure_to_qbs_def
by (rule Abs_quasi_borel_inverse) (simp add: R_Mx_correct R_qbs_closed1 R_qbs_closed2 R_qbs_closed3)
lemma qbs_space_R[simp]: "qbs_space (measure_to_qbs X) = space X"
by (simp add: qbs_space_def)
lemma qbs_Mx_R[simp]: "qbs_Mx (measure_to_qbs X) = real_borel ââ©M X"
by (simp add: qbs_Mx_def)
text â¹ The following lemma says that @{term measure_to_qbs} is a functor from \textbf{Meas} to \textbf{QBS}. âº
lemma r_preserves_morphisms:
"X ââ©M Y â (measure_to_qbs X) ââ©Q (measure_to_qbs Y)"
by(auto intro!: qbs_morphismI)
subsubsection â¹ The Functor $L$ âº
definition sigma_Mx :: "'a quasi_borel â 'a set set" where
"sigma_Mx X â¡ {U â© qbs_space X |U. âαâqbs_Mx X. α -` U â sets real_borel}"
definition qbs_to_measure :: "'a quasi_borel â 'a measure" where
"qbs_to_measure X â¡ Abs_measure (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A â - sigma_Mx X then 0 else â))"
lemma measure_space_L: "measure_space (qbs_space X) (sigma_Mx X) (λA. (if A = {} then 0 else if A â - sigma_Mx X then 0 else â))"
unfolding measure_space_def
proof auto
show "sigma_algebra (qbs_space X) (sigma_Mx X)"
proof(rule sigma_algebra.intro)
show "algebra (qbs_space X) (sigma_Mx X)"
proof
have "â U â sigma_Mx X. U â qbs_space X"
using sigma_Mx_def subset_iff by fastforce
thus "sigma_Mx X â Pow (qbs_space X)" by auto
next
show "{} â sigma_Mx X"
unfolding sigma_Mx_def by auto
next
fix A
fix B
assume "A â sigma_Mx X"
"B â sigma_Mx X"
then have "â Ua. A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by auto
have "â Ub. B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)"
using â¹B â sigma_Mx X⺠sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" by auto
from pa pb have [simp]:"âαâqbs_Mx X. α -` (Ua â© Ub) â sets real_borel"
by auto
from this pa pb sigma_Mx_def have [simp]:"(Ua â© Ub) â© qbs_space X â sigma_Mx X" by blast
from pa pb have [simp]:"A â© B = (Ua â© Ub) â© qbs_space X" by auto
thus "A â© B â sigma_Mx X" by simp
next
fix A
fix B
assume "A â sigma_Mx X"
"B â sigma_Mx X"
then have "â Ua. A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by auto
have "â Ub. B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)"
using â¹B â sigma_Mx X⺠sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" by auto
from pa pb have [simp]:"A - B = (Ua â© -Ub) â© qbs_space X" by auto
from pa pb have "âαâqbs_Mx X. α -`(Ua â© -Ub) â sets real_borel"
by (metis Diff_Compl double_compl sets.Diff vimage_Compl vimage_Int)
hence 1:"A - B â sigma_Mx X"
using sigma_Mx_def â¹A - B = Ua â© - Ub â© qbs_space X⺠by blast
show "âCâsigma_Mx X. finite C â§ disjoint C â§ A - B = â C"
proof
show "{A - B} âsigma_Mx X â§ finite {A-B} â§ disjoint {A-B} â§ A - B = â {A-B}"
using 1 by auto
qed
next
fix A
fix B
assume "A â sigma_Mx X"
"B â sigma_Mx X"
then have "â Ua. A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by auto
have "â Ub. B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)"
using â¹B â sigma_Mx X⺠sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" by auto
from pa pb have "A ⪠B = (Ua ⪠Ub) ⩠qbs_space X" by auto
from pa pb have "âαâqbs_Mx X. α -`(Ua ⪠Ub) â sets real_borel" by auto
then show "A ⪠B â sigma_Mx X"
unfolding sigma_Mx_def
using â¹A ⪠B = (Ua ⪠Ub) â© qbs_space X⺠by blast
next
have "âαâqbs_Mx X. α -` (UNIV) â sets real_borel"
by simp
thus "qbs_space X â sigma_Mx X"
unfolding sigma_Mx_def
by blast
qed
next
show "sigma_algebra_axioms (sigma_Mx X)"
unfolding sigma_algebra_axioms_def
proof(auto)
fix A :: "nat â _"
assume 1:"range A â sigma_Mx X"
then have 2:"âi. âUi. A i = Ui â© qbs_space X â§ (âαâqbs_Mx X. α -` Ui â sets real_borel)"
unfolding sigma_Mx_def by auto
then have "â U :: nat â _. âi. A i = U i â© qbs_space X â§ (âαâqbs_Mx X. α -` (U i) â sets real_borel)"
by (rule choice)
from this obtain U where pu:"âi. A i = U i â© qbs_space X â§ (âαâqbs_Mx X. α -` (U i) â sets real_borel)"
by auto
hence "âαâqbs_Mx X. α -` (â (range U)) â sets real_borel"
by (simp add: countable_Un_Int(1) vimage_UN)
from pu have "â (range A) = (âi::nat. (U i â© qbs_space X))" by blast
hence "â (range A) = â (range U) â© qbs_space X" by auto
thus "â (range A) â sigma_Mx X"
using sigma_Mx_def â¹âαâqbs_Mx X. α -` â (range U) â sets real_borel⺠by blast
qed
qed
next
show "countably_additive (sigma_Mx X) (λA. if A = {} then 0 else if A â - sigma_Mx X then 0 else â)"
proof(rule countably_additiveI)
fix A :: "nat â _"
assume h:"range A â sigma_Mx X"
"â (range A) â sigma_Mx X"
consider "â (range A) = {}" | "â (range A) â {}"
by auto
then show "(âi. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) =
(if â (range A) = {} then 0 else if â (range A) â - sigma_Mx X then 0 else (â :: ennreal))"
proof cases
case 1
then have "âi. A i = {}"
by simp
thus ?thesis
by(simp add: 1)
next
case 2
then obtain j where hj:"A j â {}"
by auto
have "(âi. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) = (â :: ennreal)"
proof -
have hsum:"âN f. sum f {..<N} ⤠(ân. (f n :: ennreal))"
by (simp add: sum_le_suminf)
have hsum':"âP f. (âj. j â P â§ f j = (â :: ennreal)) â¹ finite P â¹ sum f P = â"
by auto
have h1:"(âi<j+1. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) = (â :: ennreal)"
proof(rule hsum')
show "âja. ja â {..<j + 1} â§ (if A ja = {} then 0 else if A ja â - sigma_Mx X then 0 else â) = (â :: ennreal)"
proof(rule exI[where x=j],rule conjI)
have "A j â sigma_Mx X"
using h(1) by auto
then show "(if A j = {} then 0 else if A j â - sigma_Mx X then 0 else â) = (â :: ennreal)"
using hj by simp
qed simp
qed simp
have "(âi<j+1. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) ⤠(âi. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else (â :: ennreal))"
by(rule hsum)
thus ?thesis
by(simp only: h1) (simp add: top.extremum_unique)
qed
moreover have "(if â (range A) = {} then 0 else if â (range A) â - sigma_Mx X then 0 else â) = (â :: ennreal)"
using 2 h(2) by simp
ultimately show ?thesis
by simp
qed
qed
qed(simp add: positive_def)
lemma L_correct[simp]:"Rep_measure (qbs_to_measure X) = (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A â - sigma_Mx X then 0 else â))"
unfolding qbs_to_measure_def
by(auto intro!: Abs_measure_inverse simp: measure_space_L)
lemma space_L[simp]: "space (qbs_to_measure X) = qbs_space X"
by (simp add: space_def)
lemma sets_L[simp]: "sets (qbs_to_measure X) = sigma_Mx X"
by (simp add: sets_def)
lemma emeasure_L[simp]: "emeasure (qbs_to_measure X) = (λA. if A = {} ⨠A â sigma_Mx X then 0 else â)"
by(auto simp: emeasure_def)
lemma qbs_Mx_sigma_Mx_contra:
assumes "qbs_space X = qbs_space Y"
and "qbs_Mx X â qbs_Mx Y"
shows "sigma_Mx Y â sigma_Mx X"
using assms by(auto simp: sigma_Mx_def)
text â¹ The following lemma says that @{term qbs_to_measure} is a functor from \textbf{QBS} to \textbf{Meas}. âº
lemma l_preserves_morphisms:
"X ââ©Q Y â (qbs_to_measure X) ââ©M (qbs_to_measure Y)"
proof(auto)
fix f
assume h:"f â X ââ©Q Y"
show "f â (qbs_to_measure X) ââ©M (qbs_to_measure Y)"
proof(rule measurableI)
fix x
assume "x â space (qbs_to_measure X)"
then show "f x â space (qbs_to_measure Y)"
using h by auto
next
fix A
assume "A â sets (qbs_to_measure Y)"
then obtain Ua where pa:"A = Ua â© qbs_space Y â§ (âαâqbs_Mx Y. α -` Ua â sets real_borel)"
by (auto simp: sigma_Mx_def)
have "âαâqbs_Mx X. f â α â qbs_Mx Y"
"âαâ qbs_Mx X. α -` (f -` (qbs_space Y)) = UNIV"
using h by auto
hence "âαâqbs_Mx X. α -` (f -` A) = α -` (f -` Ua)"
by (simp add: pa)
from pa this qbs_morphism_def have "âαâqbs_Mx X. α -` (f -` A) â sets real_borel"
by (simp add: vimage_comp â¹âαâqbs_Mx X. f â α â qbs_Mx Yâº)
thus "f -` A â© space (qbs_to_measure X) â sets (qbs_to_measure X)"
using sigma_Mx_def by auto
qed
qed
abbreviation "qbs_borel â¡ measure_to_qbs borel"
declare [[coercion measure_to_qbs]]
abbreviation real_quasi_borel :: "real quasi_borel" ("ââ©Q") where
"real_quasi_borel â¡ qbs_borel"
abbreviation nat_quasi_borel :: "nat quasi_borel" ("ââ©Q") where
"nat_quasi_borel â¡ qbs_borel"
abbreviation ennreal_quasi_borel :: "ennreal quasi_borel" ("ââ©Qâ©â¥â©0") where
"ennreal_quasi_borel â¡ qbs_borel"
abbreviation bool_quasi_borel :: "bool quasi_borel" ("ð¹â©Q") where
"bool_quasi_borel â¡ qbs_borel"
lemma qbs_Mx_is_morphisms:
"qbs_Mx X = real_quasi_borel ââ©Q X"
proof(auto)
fix α
assume "α â qbs_Mx X"
then have "α â UNIV â qbs_space X â§ (â f â real_borel ââ©M real_borel. α â f â qbs_Mx X)"
by fastforce
thus "α â real_quasi_borel ââ©Q X"
by(simp add: qbs_morphism_def)
next
fix α
assume "α â real_quasi_borel ââ©Q X"
have "id â qbs_Mx real_quasi_borel" by simp
then have "α â id â qbs_Mx X"
using â¹Î± â real_quasi_borel ââ©Q X⺠qbs_morphism_def[of real_quasi_borel X]
by blast
then show "α â qbs_Mx X" by simp
qed
lemma qbs_Mx_subset_of_measurable:
"qbs_Mx X â real_borel ââ©M qbs_to_measure X"
proof
fix α
assume "α â qbs_Mx X"
show "α â real_borel ââ©M qbs_to_measure X"
proof(rule measurableI)
fix x
show "α x â space (qbs_to_measure X)"
using qbs_decomp â¹Î± â qbs_Mx X⺠by auto
next
fix A
assume "A â sets (qbs_to_measure X)"
then have "α -`(qbs_space X) = UNIV"
using â¹Î± â qbs_Mx X⺠qbs_decomp by auto
then show "α -` A â© space real_borel â sets real_borel"
using â¹Î± â qbs_Mx X⺠â¹A â sets (qbs_to_measure X)âº
by(auto simp add: sigma_Mx_def)
qed
qed
lemma L_max_of_measurables:
assumes "space M = qbs_space X"
and "qbs_Mx X â real_borel ââ©M M"
shows "sets M â sets (qbs_to_measure X)"
proof
fix U
assume "U â sets M"
from sets.sets_into_space[OF this] in_mono[OF assms(2)] measurable_sets_borel[OF _ this]
show "U â sets (qbs_to_measure X)"
using assms(1)
by(auto intro!: exI[where x=U] simp: sigma_Mx_def)
qed
lemma qbs_Mx_are_measurable[simp,measurable]:
assumes "α â qbs_Mx X"
shows "α â real_borel ââ©M qbs_to_measure X"
using assms qbs_Mx_subset_of_measurable by auto
lemma measure_to_qbs_cong_sets:
assumes "sets M = sets N"
shows "measure_to_qbs M = measure_to_qbs N"
by(rule qbs_eqI) (simp add: measurable_cong_sets[OF _ assms])
lemma lr_sets[simp,measurable_cong]:
"sets X â sets (qbs_to_measure (measure_to_qbs X))"
proof auto
fix U
assume "U â sets X"
then have "U â© space X = U" by simp
moreover have "âαâreal_borel ââ©M X. α -` U â sets real_borel"
using â¹U â sets X⺠by(auto simp add: measurable_def)
ultimately show "U â sigma_Mx (measure_to_qbs X)"
by(auto simp add: sigma_Mx_def)
qed
lemma(in standard_borel) standard_borel_lr_sets_ident[simp, measurable_cong]:
"sets (qbs_to_measure (measure_to_qbs M)) = sets M"
proof auto
fix V
assume "V â sigma_Mx (measure_to_qbs M)"
then obtain U where H2: "V = U â© space M â§ (âαâreal_borel ââ©M M. α -` U â sets real_borel)"
by(auto simp: sigma_Mx_def)
hence "g -` V = g -` (U â© space M)" by auto
have "... = g -` U" using g_meas by(auto simp add: measurable_def)
hence "f -` g -` U â© space M â sets M"
by (meson f_meas g_meas measurable_sets H2)
moreover have "f -` g -` U â© space M = U â© space M"
by auto
ultimately show "V â sets M" using H2 by simp
next
fix U
assume "U â sets M"
then show "U â sigma_Mx (measure_to_qbs M)"
using lr_sets by auto
qed
subsubsection â¹ The Adjunction âº
lemma lr_adjunction_correspondence :
"X ââ©Q (measure_to_qbs Y) = (qbs_to_measure X) ââ©M Y"
proof(auto)
fix f
assume "f â X ââ©Q (measure_to_qbs Y)"
show "f â qbs_to_measure X ââ©M Y"
proof(rule measurableI)
fix x
assume "x â space (qbs_to_measure X)"
hence "x â qbs_space X" by simp
thus "f x â space Y"
using â¹f â X ââ©Q (measure_to_qbs Y)⺠qbs_morphismE[of f X "measure_to_qbs Y"]
by auto
next
fix A
assume "A â sets Y"
have "âα â qbs_Mx X. f â α â qbs_Mx (measure_to_qbs Y)"
using â¹f â X ââ©Q (measure_to_qbs Y)⺠by auto
hence "âα â qbs_Mx X. f â α â real_borel ââ©M Y" by simp
hence "âα â qbs_Mx X. α -` (f -` A) â sets real_borel"
using â¹Aâ sets Y⺠measurable_sets_borel vimage_comp by metis
thus "f -` A â© space (qbs_to_measure X) â sets (qbs_to_measure X)"
using sigma_Mx_def by auto
qed
next
fix f
assume "f â qbs_to_measure X ââ©M Y"
show "f â X ââ©Q measure_to_qbs Y"
proof(rule qbs_morphismI,simp)
fix α
assume "α â qbs_Mx X"
show "f â α â real_borel ââ©M Y"
proof(rule measurableI)
fix x
assume "x â space real_borel"
from this â¹Î± â qbs_Mx X âºqbs_decomp have "α x â qbs_space X" by auto
hence "α x â space (qbs_to_measure X)" by simp
thus "(f â α) x â space Y"
using â¹f â qbs_to_measure X ââ©M Yâº
by (metis comp_def measurable_space)
next
fix A
assume "A â sets Y"
from â¹f â qbs_to_measure X ââ©M Y⺠measurable_sets this measurable_def
have "f -` A â© space (qbs_to_measure X) â sets (qbs_to_measure X)"
by blast
hence "f -` A â© qbs_space X â sigma_Mx X" by simp
then have "â V. f -` A â© qbs_space X = V â© qbs_space X â§ (âβâ qbs_Mx X. β -` V â sets real_borel)"
by (simp add:sigma_Mx_def)
then obtain V where h:"f -` A â© qbs_space X = V â© qbs_space X â§ (âβâ qbs_Mx X. β -` V â sets real_borel)" by auto
have 1:"α -` (f -` A) = α -` (f -` A ⩠qbs_space X)"
using â¹Î± â qbs_Mx X⺠by blast
have 2:"α -` (V ⩠qbs_space X) = α -` V"
using â¹Î± â qbs_Mx X⺠by blast
from 1 2 h have "(f â α) -` A = α -` V" by (simp add: vimage_comp)
from this h â¹Î± â qbs_Mx X âºshow "(f â α) -` A â© space real_borel â sets real_borel" by simp
qed
qed
qed
lemma(in standard_borel) standard_borel_r_full_faithful:
"M ââ©M Y = measure_to_qbs M ââ©Q measure_to_qbs Y"
proof(standard;standard)
fix h
assume "h â M ââ©M Y"
then show "h â measure_to_qbs M ââ©Q measure_to_qbs Y"
using r_preserves_morphisms by auto
next
fix h
assume h:"h â measure_to_qbs M ââ©Q measure_to_qbs Y"
show "h â M ââ©M Y"
proof(rule measurableI)
fix x
assume "x â space M"
then show "h x â space Y"
using h by auto
next
fix U
assume "U â sets Y"
have "h â g â real_borel ââ©M Y"
using â¹h â measure_to_qbs M ââ©Q measure_to_qbs Yâº
by(simp add: qbs_morphism_def)
hence "(h â g) -` U â sets real_borel"
by (simp add: â¹U â sets Y⺠measurable_sets_borel)
hence "f -` ((h â g) -` U) â© space M â sets M"
using f_meas in_borel_measurable_borel by blast
moreover have "f -` ((h â g) -` U) â© space M = h -` U â© space M"
using f_meas by auto
ultimately show "h -` U â© space M â sets M" by simp
qed
qed
lemma qbs_morphism_dest[dest]:
assumes "f â X ââ©Q measure_to_qbs Y"
shows "f â qbs_to_measure X ââ©M Y"
using assms lr_adjunction_correspondence by auto
lemma(in standard_borel) qbs_morphism_dest[dest]:
assumes "k â measure_to_qbs M ââ©Q measure_to_qbs Y"
shows "k â M ââ©M Y"
using standard_borel_r_full_faithful assms by auto
lemma qbs_morphism_measurable_intro[intro!]:
assumes "f â qbs_to_measure X ââ©M Y"
shows "f â X ââ©Q measure_to_qbs Y"
using assms lr_adjunction_correspondence by auto
lemma(in standard_borel) qbs_morphism_measurable_intro[intro!]:
assumes "k â M ââ©M Y"
shows "k â measure_to_qbs M ââ©Q measure_to_qbs Y"
using standard_borel_r_full_faithful assms by auto
text â¹ We can use the measurability prover when we reason about morphisms. âº
lemma
assumes "f â ââ©Q ââ©Q ââ©Q"
shows "(λx. 2 * f x + (f x)^2) â ââ©Q ââ©Q ââ©Q"
using assms by auto
lemma
assumes "f â X ââ©Q ââ©Q"
and "α â qbs_Mx X"
shows "(λx. 2 * f (α x) + (f (α x))^2) â ââ©Q ââ©Q ââ©Q"
using assms by auto
lemma qbs_morphisn_from_countable:
fixes X :: "'a quasi_borel"
assumes "countable (qbs_space X)"
"qbs_Mx X â real_borel ââ©M count_space (qbs_space X)"
and "âi. i â qbs_space X â¹ f i â qbs_space Y"
shows "f â X ââ©Q Y"
proof(rule qbs_morphismI)
fix α
assume "α â qbs_Mx X"
then have [measurable]: "α â real_borel ââ©M count_space (qbs_space X)"
using assms(2) ..
define k :: "'a â real â _"
where "k ⡠(λi _. f i)"
have "f â α = (λr. k (α r) r)"
by(auto simp add: k_def)
also have "... â qbs_Mx Y"
by(rule qbs_closed3_dest2[OF assms(1)]) (use assms(3) k_def in simp_all)
finally show "f â α â qbs_Mx Y" .
qed
corollary nat_qbs_morphism:
assumes "ân. f n â qbs_space Y"
shows "f â ââ©Q ââ©Q Y"
using assms measurable_cong_sets[OF refl sets_borel_eq_count_space,of real_borel]
by(auto intro!: qbs_morphisn_from_countable)
corollary bool_qbs_morphism:
assumes "âb. f b â qbs_space Y"
shows "f â ð¹â©Q ââ©Q Y"
using assms measurable_cong_sets[OF refl sets_borel_eq_count_space,of real_borel]
by(auto intro!: qbs_morphisn_from_countable)
subsubsection â¹ The Adjunction w.r.t. Orderingâº
lemma l_mono:
"mono qbs_to_measure"
apply standard
subgoal for X Y
proof(induction rule: less_eq_quasi_borel.induct)
case (1 X Y)
then show ?case
by(simp add: less_eq_measure.intros(1))
next
case (2 X Y)
then have "sigma_Mx X â sigma_Mx Y"
by(auto simp add: sigma_Mx_def)
then consider "sigma_Mx X â sigma_Mx Y" | "sigma_Mx X = sigma_Mx Y"
by auto
then show ?case
apply(cases)
apply(rule less_eq_measure.intros(2))
apply(simp_all add: 2)
by(rule less_eq_measure.intros(3),simp_all add: 2)
qed
done
lemma r_mono:
"mono measure_to_qbs"
apply standard
subgoal for M N
proof(induction rule: less_eq_measure.inducts)
case (1 M N)
then show ?case
by(simp add: less_eq_quasi_borel.intros(1))
next
case (2 M N)
then have "real_borel ââ©M N â real_borel ââ©M M"
by(simp add: measurable_mono)
then consider "real_borel ââ©M N â real_borel ââ©M M" | "real_borel ââ©M N = real_borel ââ©M M"
by auto
then show ?case
by cases (rule less_eq_quasi_borel.intros(2),simp_all add: 2)+
next
case (3 M N)
then show ?case
apply -
by(rule less_eq_quasi_borel.intros(2)) (simp_all add: measurable_mono)
qed
done
lemma rl_order_adjunction:
"X ⤠qbs_to_measure Y ⷠmeasure_to_qbs X ⤠Y"
proof
assume 1: "X ⤠qbs_to_measure Y"
then show "measure_to_qbs X ⤠Y"
proof(induction rule: less_eq_measure.cases)
case (1 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 1(2)[symmetric])
show ?case
by(rule less_eq_quasi_borel.intros(1),simp add: 1)
next
case (2 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 2(2)[symmetric])
show ?case
proof(rule less_eq_quasi_borel.intros(2),simp add:2,auto)
fix α
assume h:"α â qbs_Mx Y"
show "α â real_borel ââ©M X"
proof(rule measurableI,simp_all)
show "âx. α x â space X"
using h by (auto simp add: 2)
next
fix A
assume "A â sets X"
then have "A â sets (qbs_to_measure Y)"
using 2 by auto
then obtain U where
hu:"A = U â© space N"
"(âαâqbs_Mx Y. α -` U â sets real_borel)"
by(auto simp add: sigma_Mx_def)
have "α -` A = α -` U"
using h qbs_decomp[of Y]
by(auto simp add: hu)
thus "α -` A â sets borel"
using h hu(2) by simp
qed
qed
next
case (3 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 3(2)[symmetric])
show ?case
proof(rule less_eq_quasi_borel.intros(2),simp add: 3,auto)
fix α
assume h:"α â qbs_Mx Y"
show "α â real_borel ââ©M X"
proof(rule measurableI,simp_all)
show "âx. α x â space X"
using h by(auto simp: 3)
next
fix A
assume "A â sets X"
then have "A â sets (qbs_to_measure Y)"
using 3 by auto
then obtain U where
hu:"A = U â© space N"
"(âαâqbs_Mx Y. α -` U â sets real_borel)"
by(auto simp add: sigma_Mx_def)
have "α -` A = α -` U"
using h qbs_decomp[of Y]
by(auto simp add: hu)
thus "α -` A â sets borel"
using h hu(2) by simp
qed
qed
qed
next
assume "measure_to_qbs X ⤠Y"
then show "X ⤠qbs_to_measure Y"
proof(induction rule: less_eq_quasi_borel.cases)
case (1 A B)
have [simp]: "space X = qbs_space A"
by(simp add: 1(1)[symmetric])
show ?case
by(rule less_eq_measure.intros(1)) (simp add: 1)
next
case (2 A B)
then have hmy:"qbs_Mx Y â real_borel ââ©M X"
by auto
have [simp]: "space X = qbs_space A"
by(simp add: 2(1)[symmetric])
have "sets X â sigma_Mx Y"
proof
fix U
assume hu:"U â sets X"
show "U â sigma_Mx Y"
proof(simp add: sigma_Mx_def,rule exI[where x=U],auto)
show "âx. x â U â¹ x â qbs_space Y"
using sets.sets_into_space[OF hu]
by(auto simp add: 2)
next
fix α
assume "α â qbs_Mx Y"
then have "α â real_borel ââ©M X"
using hmy by(auto)
thus "α -` U â sets real_borel"
using hu by(simp add: measurable_sets_borel)
qed
qed
then consider "sets X = sigma_Mx Y" | "sets X â sigma_Mx Y"
by auto
then show ?case
proof cases
case 1
show ?thesis
apply(rule less_eq_measure.intros(3),simp_all add: 1 2)
proof(rule le_funI)
fix U
consider "U = {}" | "U â sigma_Mx B" | "U â {} â§ U â sigma_Mx B"
by auto
then show "emeasure X U ⤠(if U = {} ⨠U â sigma_Mx B then 0 else â)"
proof cases
case 1
then show ?thesis by simp
next
case h:2
then have "U â sigma_Mx A"
using qbs_Mx_sigma_Mx_contra[OF 2(3)[symmetric] 2(4)]
by auto
hence "U â sets X"
using lr_sets 2(1) by auto
thus ?thesis
by(simp add: h emeasure_notin_sets)
next
case 3
then show ?thesis
by simp
qed
qed
next
case h2:2
show ?thesis
by(rule less_eq_measure.intros(2)) (simp add: 2,simp add: h2)
qed
qed
qed
end
Theory Binary_Product_QuasiBorel
subsection â¹Product Spacesâº
theory Binary_Product_QuasiBorel
imports "Measure_QuasiBorel_Adjunction"
begin
subsubsection â¹ Binary Product Spaces âº
definition pair_qbs_Mx :: "['a quasi_borel, 'b quasi_borel] â (real => 'a à 'b) set" where
"pair_qbs_Mx X Y â¡ {f. fst â f â qbs_Mx X â§ snd â f â qbs_Mx Y}"
definition pair_qbs :: "['a quasi_borel, 'b quasi_borel] â ('a à 'b) quasi_borel" (infixr "â¨â©Q" 80) where
"pair_qbs X Y = Abs_quasi_borel (qbs_space X Ã qbs_space Y, pair_qbs_Mx X Y)"
lemma pair_qbs_f[simp]: "pair_qbs_Mx X Y â UNIV â qbs_space X Ã qbs_space Y"
unfolding pair_qbs_Mx_def
by (auto simp: mem_Times_iff[of _ "qbs_space X" "qbs_space Y"]; fastforce)
lemma pair_qbs_closed1: "qbs_closed1 (pair_qbs_Mx (X::'a quasi_borel) (Y::'b quasi_borel))"
unfolding pair_qbs_Mx_def qbs_closed1_def
by (metis (no_types, lifting) comp_assoc mem_Collect_eq qbs_closed1_dest)
lemma pair_qbs_closed2: "qbs_closed2 (qbs_space X Ã qbs_space Y) (pair_qbs_Mx X Y)"
unfolding qbs_closed2_def pair_qbs_Mx_def
by auto
lemma pair_qbs_closed3: "qbs_closed3 (pair_qbs_Mx (X::'a quasi_borel) (Y::'b quasi_borel))"
proof(auto simp add: qbs_closed3_def pair_qbs_Mx_def)
fix P :: "real â nat"
fix Fi :: "nat â real â 'a à 'b"
define Fj :: "nat â real â 'a" where "Fj ⡠λj.(fst â Fi j)"
assume "âi. fst â Fi i â qbs_Mx X â§ snd â Fi i â qbs_Mx Y"
then have "âi. Fj i â qbs_Mx X" by (simp add: Fj_def)
moreover assume "âi. P -` {i} â sets real_borel"
ultimately have "(λr. Fj (P r) r) â qbs_Mx X"
by auto
moreover have "fst â (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def)
ultimately show "fst â (λr. Fi (P r) r) â qbs_Mx X" by simp
next
fix P :: "real â nat"
fix Fi :: "nat â real â 'a à 'b"
define Fj :: "nat â real â 'b" where "Fj ⡠λj.(snd â Fi j)"
assume "âi. fst â Fi i â qbs_Mx X â§ snd â Fi i â qbs_Mx Y"
then have "âi. Fj i â qbs_Mx Y" by (simp add: Fj_def)
moreover assume "âi. P -` {i} â sets real_borel"
ultimately have "(λr. Fj (P r) r) â qbs_Mx Y"
by auto
moreover have "snd â (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def)
ultimately show "snd â (λr. Fi (P r) r) â qbs_Mx Y" by simp
qed
lemma pair_qbs_correct: "Rep_quasi_borel (X â¨â©Q Y) = (qbs_space X à qbs_space Y, pair_qbs_Mx X Y)"
unfolding pair_qbs_def
by(auto intro!: Abs_quasi_borel_inverse pair_qbs_f simp: pair_qbs_closed3 pair_qbs_closed2 pair_qbs_closed1)
lemma pair_qbs_space[simp]: "qbs_space (X â¨â©Q Y) = qbs_space X à qbs_space Y"
by (simp add: qbs_space_def pair_qbs_correct)
lemma pair_qbs_Mx[simp]: "qbs_Mx (X â¨â©Q Y) = pair_qbs_Mx X Y"
by (simp add: qbs_Mx_def pair_qbs_correct)
lemma pair_qbs_morphismI:
assumes "âα β. α â qbs_Mx X ⹠β â qbs_Mx Y
â¹ f â (λr. (α r, β r)) â qbs_Mx Z"
shows "f â (X â¨â©Q Y) ââ©Q Z"
proof(rule qbs_morphismI)
fix α
assume 1:"α â qbs_Mx (X â¨â©Q Y)"
have "f â α = f â (λr. ((fst â α) r, (snd â α) r))"
by auto
also have "... â qbs_Mx Z"
using 1 assms[of "fst â α" "snd â α"]
by(simp add: pair_qbs_Mx_def)
finally show "f â α â qbs_Mx Z" .
qed
lemma fst_qbs_morphism:
"fst â X â¨â©Q Y ââ©Q X"
by(auto simp add: qbs_morphism_def pair_qbs_Mx_def)
lemma snd_qbs_morphism:
"snd â X â¨â©Q Y ââ©Q Y"
by(auto simp add: qbs_morphism_def pair_qbs_Mx_def)
lemma qbs_morphism_pair_iff:
"f â X ââ©Q Y â¨â©Q Z â· fst â f â X ââ©Q Y â§ snd â f â X ââ©Q Z"
by(auto intro!: qbs_morphismI qbs_morphism_comp[OF _ fst_qbs_morphism,of f X Y Z ]qbs_morphism_comp[OF _ snd_qbs_morphism,of f X Y Z]
simp: pair_qbs_Mx_def comp_assoc[symmetric])
lemma qbs_morphism_Pair1:
assumes "x â qbs_space X"
shows "Pair x â Y ââ©Q X â¨â©Q Y"
using assms
by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def comp_def)
lemma qbs_morphism_Pair1':
assumes "x â qbs_space X"
and "f â X â¨â©Q Y ââ©Q Z"
shows "(λy. f (x,y)) â Y ââ©Q Z"
using qbs_morphism_comp[OF qbs_morphism_Pair1[OF assms(1)] assms(2)]
by(simp add: comp_def)
lemma qbs_morphism_Pair2:
assumes "y â qbs_space Y"
shows "(λx. (x,y)) â X ââ©Q X â¨â©Q Y"
using assms
by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def comp_def)
lemma qbs_morphism_Pair2':
assumes "y â qbs_space Y"
and "f â X â¨â©Q Y ââ©Q Z"
shows "(λx. f (x,y)) â X ââ©Q Z"
using qbs_morphism_comp[OF qbs_morphism_Pair2[OF assms(1)] assms(2)]
by(simp add: comp_def)
lemma qbs_morphism_fst'':
assumes "f â X ââ©Q Y"
shows "(λk. f (fst k)) â X â¨â©Q Z ââ©Q Y"
using qbs_morphism_comp[OF fst_qbs_morphism assms,of Z]
by(simp add: comp_def)
lemma qbs_morphism_snd'':
assumes "f â X ââ©Q Y"
shows "(λk. f (snd k)) â Z â¨â©Q X ââ©Q Y"
using qbs_morphism_comp[OF snd_qbs_morphism assms,of Z]
by(simp add: comp_def)
lemma qbs_morphism_tuple:
assumes "f â Z ââ©Q X"
and "g â Z ââ©Q Y"
shows "(λz. (f z, g z)) â Z ââ©Q X â¨â©Q Y"
proof(rule qbs_morphismI,simp)
fix α
assume h:"α â qbs_Mx Z"
then have "(λz. (f z, g z)) â α â UNIV â qbs_space X à qbs_space Y"
using assms qbs_morphismE(2)[OF assms(1)] qbs_morphismE(2)[OF assms(2)]
by fastforce
moreover have "fst â ((λz. (f z, g z)) â α) = f â α" by auto
moreover have "... â qbs_Mx X"
using assms(1) h by auto
moreover have "snd â ((λz. (f z, g z)) â α) = g â α" by auto
moreover have "... â qbs_Mx Y"
using assms(2) h by auto
ultimately show "(λz. (f z, g z)) â α â pair_qbs_Mx X Y"
by (simp add: pair_qbs_Mx_def)
qed
lemma qbs_morphism_map_prod:
assumes "f â X ââ©Q Y"
and "g â X' ââ©Q Y'"
shows "map_prod f g â X â¨â©Q X'ââ©Q Y â¨â©Q Y'"
proof(rule pair_qbs_morphismI)
fix α β
assume h:"α â qbs_Mx X"
"β â qbs_Mx X'"
have [simp]: "fst â (map_prod f g â (λr. (α r, β r))) = f â α" by auto
have [simp]: "snd â (map_prod f g â (λr. (α r, β r))) = g â β" by auto
show "map_prod f g â (λr. (α r, β r)) â qbs_Mx (Y â¨â©Q Y')"
using h assms by(auto simp: pair_qbs_Mx_def)
qed
lemma qbs_morphism_pair_swap':
"(λ(x,y). (y,x)) â (X::'a quasi_borel) â¨â©Q (Y::'b quasi_borel) ââ©Q Y â¨â©Q X"
by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def)
lemma qbs_morphism_pair_swap:
assumes "f â X â¨â©Q Y ââ©Q Z"
shows "(λ(x,y). f (y,x)) â Y â¨â©Q X ââ©Q Z"
proof -
have "(λ(x,y). f (y,x)) = f â (λ(x,y). (y,x))" by auto
thus ?thesis
using qbs_morphism_comp[of "(λ(x,y). (y,x))" "Y â¨â©Q X" _ f] qbs_morphism_pair_swap' assms
by auto
qed
lemma qbs_morphism_pair_assoc1:
"(λ((x,y),z). (x,(y,z))) â (X â¨â©Q Y) â¨â©Q Z ââ©Q X â¨â©Q (Y â¨â©Q Z)"
by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def)
lemma qbs_morphism_pair_assoc2:
"(λ(x,(y,z)). ((x,y),z)) â X â¨â©Q (Y â¨â©Q Z) ââ©Q (X â¨â©Q Y) â¨â©Q Z"
by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def)
lemma pair_qbs_fst:
assumes "qbs_space Y â {}"
shows "map_qbs fst (X â¨â©Q Y) = X"
proof(rule qbs_eqI)
show "qbs_Mx (map_qbs fst (X â¨â©Q Y)) = qbs_Mx X"
proof auto
fix αx
assume hx:"αx â qbs_Mx X"
obtain αy where hy:"αy â qbs_Mx Y"
using qbs_empty_equiv[of Y] assms
by auto
show "âαâpair_qbs_Mx X Y. αx = fst â α"
by(auto intro!: exI[where x="λr. (αx r, αy r)"] simp: pair_qbs_Mx_def hx hy comp_def)
qed (simp add: pair_qbs_Mx_def)
qed
lemma pair_qbs_snd:
assumes "qbs_space X â {}"
shows "map_qbs snd (X â¨â©Q Y) = Y"
proof(rule qbs_eqI)
show "qbs_Mx (map_qbs snd (X â¨â©Q Y)) = qbs_Mx Y"
proof auto
fix αy
assume hy:"αy â qbs_Mx Y"
obtain αx where hx:"αx â qbs_Mx X"
using qbs_empty_equiv[of X] assms
by auto
show "âαâpair_qbs_Mx X Y. αy = snd â α"
by(auto intro!: exI[where x="λr. (αx r, αy r)"] simp: pair_qbs_Mx_def hx hy comp_def)
qed (simp add: pair_qbs_Mx_def)
qed
text â¹ The following lemma corresponds to \cite{Heunen_2017} Proposition 19(1). âº
lemma r_preserves_product :
"measure_to_qbs (X â¨â©M Y) = measure_to_qbs X â¨â©Q measure_to_qbs Y"
by(auto intro!: qbs_eqI simp: measurable_pair_iff pair_qbs_Mx_def)
lemma l_product_sets[simp,measurable_cong]:
"sets (qbs_to_measure X â¨â©M qbs_to_measure Y) â sets (qbs_to_measure (X â¨â©Q Y))"
proof(rule sets_pair_in_sets,simp)
fix A B
assume h:"A â sigma_Mx X"
"B â sigma_Mx Y"
then obtain Ua Ub where hu:
"A = Ua â© qbs_space X" "âαâqbs_Mx X. α -` Ua â sets real_borel"
"B = Ub â© qbs_space Y" "âαâqbs_Mx Y. α -` Ub â sets real_borel"
by(auto simp add: sigma_Mx_def)
show "A à B â sigma_Mx (X â¨â©Q Y)"
proof(simp add: sigma_Mx_def, rule exI[where x="Ua à Ub"])
show "A à B = Ua à Ub â© qbs_space X à qbs_space Y â§
(âαâpair_qbs_Mx X Y. α -` (Ua à Ub) â sets real_borel)"
using hu by(auto simp add: pair_qbs_Mx_def vimage_Times)
qed
qed
lemma(in pair_standard_borel) l_r_r_sets[simp,measurable_cong]:
"sets (qbs_to_measure (measure_to_qbs M â¨â©Q measure_to_qbs N)) = sets (M â¨â©M N)"
by(simp only: r_preserves_product[symmetric]) (rule standard_borel_lr_sets_ident)
end
Theory Product_QuasiBorel
subsubsection â¹ Product Spacesâº
theory Product_QuasiBorel
imports "Binary_Product_QuasiBorel"
begin
definition prod_qbs_Mx :: "['a set, 'a â 'b quasi_borel] â (real â 'a â 'b) set" where
"prod_qbs_Mx I M â¡ { α | α. âi. (i â I â¶ (λr. α r i) â qbs_Mx (M i)) â§ (i â I â¶ (λr. α r i) = (λr. undefined))}"
lemma prod_qbs_MxI:
assumes "âi. i â I â¹ (λr. α r i) â qbs_Mx (M i)"
and "âi. i â I â¹ (λr. α r i) = (λr. undefined)"
shows "α â prod_qbs_Mx I M"
using assms by(auto simp: prod_qbs_Mx_def)
lemma prod_qbs_MxE:
assumes "α â prod_qbs_Mx I M"
shows "âi. i â I â¹ (λr. α r i) â qbs_Mx (M i)"
and "âi. i â I â¹ (λr. α r i) = (λr. undefined)"
and "âi r. i â I ⹠α r i = undefined"
using assms by(auto simp: prod_qbs_Mx_def dest: fun_cong[where g="(λr. undefined)"])
definition PiQ :: "'a set â ('a â 'b quasi_borel) â ('a â 'b) quasi_borel" where
"PiQ I M â¡ Abs_quasi_borel (Î â©E iâI. qbs_space (M i), prod_qbs_Mx I M)"
syntax
"_PiQ" :: "pttrn â 'i set â 'a quasi_borel â ('i => 'a) quasi_borel" ("(3Î â©Q _â_./ _)" 10)
translations
"Î â©Q xâI. M" == "CONST PiQ I (λx. M)"
lemma PiQ_f: "prod_qbs_Mx I M â UNIV â (Î â©E iâI. qbs_space (M i))"
using prod_qbs_MxE by fastforce
lemma PiQ_closed1: "qbs_closed1 (prod_qbs_Mx I M)"
proof(rule qbs_closed1I)
fix α f
assume h:"α â prod_qbs_Mx I M "
"f â real_borel ââ©M real_borel"
show "α â f â prod_qbs_Mx I M"
proof(rule prod_qbs_MxI)
fix i
assume "i â I"
from prod_qbs_MxE(1)[OF h(1) this]
have "(λr. α r i) â f â qbs_Mx (M i)"
using h(2) by auto
thus "(λr. (α â f) r i) â qbs_Mx (M i)"
by(simp add: comp_def)
next
fix i
assume "i â I"
from prod_qbs_MxE(3)[OF h(1) this]
show "(λr. (α â f) r i) = (λr. undefined)"
by simp
qed
qed
lemma PiQ_closed2: "qbs_closed2 (Î â©E iâI. qbs_space (M i)) (prod_qbs_Mx I M)"
proof(rule qbs_closed2I)
fix x
assume h:"x â (Î â©E iâI. qbs_space (M i))"
show "(λr. x) â prod_qbs_Mx I M"
proof(rule prod_qbs_MxI)
fix i
assume hi:"i â I"
then have "x i â qbs_space (M i)"
using h by auto
thus "(λr. x i) â qbs_Mx (M i)"
by auto
next
show "âi. i â I â¹ (λr. x i) = (λr. undefined)"
using h by auto
qed
qed
lemma PiQ_closed3: "qbs_closed3 (prod_qbs_Mx I M)"
proof(rule qbs_closed3I)
fix P Fi
assume h:"âi::nat. P -` {i} â sets real_borel"
"âi::nat. Fi i â prod_qbs_Mx I M"
show "(λr. Fi (P r) r) â prod_qbs_Mx I M"
proof(rule prod_qbs_MxI)
fix i
assume hi:"i â I"
show "(λr. Fi (P r) r i) â qbs_Mx (M i)"
using prod_qbs_MxE(1)[OF h(2) hi] qbs_closed3_dest[OF h(1),of "λj r. Fi j r i"]
by auto
next
show "âi. i â I â¹
(λr. Fi (P r) r i) = (λr. undefined)"
using prod_qbs_MxE[OF h(2)] by auto
qed
qed
lemma PiQ_correct: "Rep_quasi_borel (PiQ I M) = (Î â©E iâI. qbs_space (M i), prod_qbs_Mx I M)"
by(auto intro!: Abs_quasi_borel_inverse PiQ_f is_quasi_borel_intro simp: PiQ_def PiQ_closed1 PiQ_closed2 PiQ_closed3)
lemma PiQ_space[simp]: "qbs_space (PiQ I M) = (Î â©E iâI. qbs_space (M i))"
by(simp add: qbs_space_def PiQ_correct)
lemma PiQ_Mx[simp]: "qbs_Mx (PiQ I M) = prod_qbs_Mx I M"
by(simp add: qbs_Mx_def PiQ_correct)
lemma qbs_morphism_component_singleton:
assumes "i â I"
shows "(λx. x i) â (Î â©Q iâI. (M i)) ââ©Q M i"
by(auto intro!: qbs_morphismI simp: prod_qbs_Mx_def comp_def assms)
lemma product_qbs_canonical1:
assumes "âi. i â I â¹ f i â Y ââ©Q X i"
and "âi. i â I â¹ f i = (λy. undefined)"
shows "(λy i. f i y) â Y ââ©Q (Î â©Q iâI. X i)"
using qbs_morphismE(3)[simplified comp_def,OF assms(1)] assms(2)
by(auto intro!: qbs_morphismI prod_qbs_MxI)
lemma product_qbs_canonical2:
assumes "âi. i â I â¹ f i â Y ââ©Q X i"
"âi. i â I â¹ f i = (λy. undefined)"
"g â Y ââ©Q (Î â©Q iâI. X i)"
"âi. i â I â¹ f i = (λx. x i) â g"
and "y â qbs_space Y"
shows "g y = (λi. f i y)"
proof(rule ext)+
fix i
show "g y i = f i y"
proof(cases "i â I")
case True
then show ?thesis
using assms(4)[of i] by simp
next
case False
moreover have "(λr. y) â qbs_Mx Y"
using assms(5) by simp
ultimately show ?thesis
using assms(2,3) qbs_morphismE(3)[OF assms(3) _]
by(fastforce simp: prod_qbs_Mx_def)
qed
qed
lemma merge_qbs_morphism:
"merge I J â (Î â©Q iâI. (M i)) â¨â©Q (Î â©Q jâJ. (M j)) ââ©Q (Î â©Q iâIâªJ. (M i))"
proof(rule qbs_morphismI)
fix α
assume h:"α â qbs_Mx ((Î â©Q iâI. (M i)) â¨â©Q (Î â©Q jâJ. (M j)))"
show "merge I J â α â qbs_Mx (Î â©Q iâIâªJ. (M i))"
proof(simp, rule prod_qbs_MxI)
fix i
assume "i â I ⪠J"
then consider "i â I" | "i â I â§ i â J" | "i â I â§ i â J"
by auto
then show "(λr. (merge I J â α) r i) â qbs_Mx (M i)"
apply cases
using h
by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE)
next
fix i
assume "i â I ⪠J"
then show "(λr. (merge I J â α) r i) = (λr. undefined)"
using h
by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE )
qed
qed
text â¹ The following lemma corresponds to \cite{Heunen_2017} Proposition 19(1). âº
lemma r_preserves_product':
"measure_to_qbs (Î â©M iâI. M i) = (Î â©Q iâI. measure_to_qbs (M i))"
proof(rule qbs_eqI)
show "qbs_Mx (measure_to_qbs (Piâ©M I M)) = qbs_Mx (Î â©Q iâI. measure_to_qbs (M i))"
proof auto
fix f
assume h:"f â real_borel ââ©M Piâ©M I M"
show "f â prod_qbs_Mx I (λi. measure_to_qbs (M i))"
proof(rule prod_qbs_MxI)
fix i
assume 1:"i â I"
show "(λr. f r i) â qbs_Mx (measure_to_qbs (M i))"
using measurable_comp[OF h measurable_component_singleton[OF 1,of M]]
by (simp add: comp_def)
next
fix i
assume 1:"i â I"
then show "(λr. f r i) = (λr. undefined)"
using measurable_space[OF h] 1
by(auto simp: space_PiM PiE_def extensional_def)
qed
next
fix f
assume h:"f â prod_qbs_Mx I (λi. measure_to_qbs (M i))"
show "f â real_borel ââ©M Piâ©M I M"
apply(rule measurable_PiM_single')
using prod_qbs_MxE(1)[OF h] apply auto[1]
using PiQ_f[of I M] h by auto
qed
qed
text â¹ $\prod_{i = 0,1} X_i \cong X_1 \times X_2$. âº
lemma product_binary_product:
"âf g. f â (Î â©Q iâUNIV. if i then X else Y) ââ©Q X â¨â©Q Y â§ g â X â¨â©Q Y ââ©Q (Î â©Q iâUNIV. if i then X else Y) â§
g â f = id â§ f â g = id"
by(auto intro!: exI[where x="λf. (f True, f False)"] exI[where x="λxy b. if b then fst xy else snd xy"] qbs_morphismI
simp: prod_qbs_Mx_def pair_qbs_Mx_def comp_def all_bool_eq ext)
end d>
Theory CoProduct_QuasiBorel
subsubsection â¹ Countable Coproduct Spaces âº
theory CoProduct_QuasiBorel
imports
"Product_QuasiBorel"
"Binary_CoProduct_QuasiBorel"
begin
definition coprod_qbs_Mx :: "['a set, 'a â 'b quasi_borel] â (real â 'a à 'b) set" where
"coprod_qbs_Mx I X â¡ { λr. (f r, α (f r) r) |f α. f â real_borel ââ©M count_space I â§ (âiârange f. α i â qbs_Mx (X i))}"
lemma coprod_qbs_MxI:
assumes "f â real_borel ââ©M count_space I"
and "âi. i â range f ⹠α i â qbs_Mx (X i)"
shows "(λr. (f r, α (f r) r)) â coprod_qbs_Mx I X"
using assms unfolding coprod_qbs_Mx_def by blast
definition coprod_qbs_Mx' :: "['a set, 'a â 'b quasi_borel] â (real â 'a à 'b) set" where
"coprod_qbs_Mx' I X â¡ { λr. (f r, α (f r) r) |f α. f â real_borel ââ©M count_space I â§ (âi. (i â range f ⨠qbs_space (X i) â {}) ⶠα i â qbs_Mx (X i))}"
lemma coproduct_qbs_Mx_eq:
"coprod_qbs_Mx I X = coprod_qbs_Mx' I X"
proof auto
fix α
assume "α â coprod_qbs_Mx I X"
then obtain f β where hfb:
"f â real_borel ââ©M count_space I"
"âi. i â range f ⹠β i â qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))"
unfolding coprod_qbs_Mx_def by blast
define β' where "β' â¡ (λi. if i â range f then β i
else if qbs_space (X i) â {} then (SOME γ. γ â qbs_Mx (X i))
else β i)"
have 1:"α = (λr. (f r, β' (f r) r))"
by(simp add: hfb(3) β'_def)
have 2:"âi. qbs_space (X i) â {} ⹠β' i â qbs_Mx (X i)"
proof -
fix i
assume hne:"qbs_space (X i) â {}"
then obtain x where "x â qbs_space (X i)" by auto
hence "(λr. x) â qbs_Mx (X i)" by auto
thus "β' i â qbs_Mx (X i)"
by(cases "i â range f") (auto simp: β'_def hfb(2) hne intro!: someI2[where a="λr. x"])
qed
show "α â coprod_qbs_Mx' I X"
using hfb(1,2) 1 2 by(auto simp: coprod_qbs_Mx'_def intro!: exI[where x=f] exI[where x=β'])
next
fix α
assume "α â coprod_qbs_Mx' I X"
then obtain f β where hfb:
"f â real_borel ââ©M count_space I" "âi. qbs_space (X i) â {} ⹠β i â qbs_Mx (X i)"
"âi. i â range f ⹠β i â qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))"
unfolding coprod_qbs_Mx'_def by blast
show "α â coprod_qbs_Mx I X"
by(auto simp: hfb(4) intro!: coprod_qbs_MxI[OF hfb(1) hfb(3)])
qed
definition coprod_qbs :: "['a set, 'a â 'b quasi_borel] â ('a à 'b) quasi_borel" where
"coprod_qbs I X â¡ Abs_quasi_borel (SIGMA i:I. qbs_space (X i), coprod_qbs_Mx I X)"
syntax
"_coprod_qbs" :: "pttrn â 'i set â 'a quasi_borel â ('i à 'a) quasi_borel" ("(3⨿â©Q _â_./ _)" 10)
translations
"⨿â©Q xâI. M" â "CONST coprod_qbs I (λx. M)"
lemma coprod_qbs_f[simp]: "coprod_qbs_Mx I X â UNIV â (SIGMA i:I. qbs_space (X i))"
by(fastforce simp: coprod_qbs_Mx_def dest: measurable_space)
lemma coprod_qbs_closed1: "qbs_closed1 (coprod_qbs_Mx I X)"
proof(rule qbs_closed1I)
fix α f
assume "α â coprod_qbs_Mx I X"
and 1[measurable]: "f â real_borel ââ©M real_borel"
then obtain β g where ha:
"âi. i â range g ⹠β i â qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and [measurable]:"g â real_borel ââ©M count_space I"
by(fastforce simp: coprod_qbs_Mx_def)
then have "âi. i â range g ⹠β i â f â qbs_Mx (X i)"
by simp
thus "α â f â coprod_qbs_Mx I X"
by(auto intro!: coprod_qbs_MxI[where f="g â f" and α="λi. β i â f",simplified comp_def] simp: ha(2) comp_def)
qed
lemma coprod_qbs_closed2: "qbs_closed2 (SIGMA i:I. qbs_space (X i)) (coprod_qbs_Mx I X)"
proof(rule qbs_closed2I,auto)
fix i x
assume "i â I" "x â qbs_space (X i)"
then show "(λr. (i,x)) â coprod_qbs_Mx I X"
by(auto simp: coprod_qbs_Mx_def intro!: exI[where x="λr. i"])
qed
lemma coprod_qbs_closed3:
"qbs_closed3 (coprod_qbs_Mx I X)"
proof(rule qbs_closed3I)
fix P Fi
assume h:"âi :: nat. P -` {i} â sets real_borel"
"âi :: nat. Fi i â coprod_qbs_Mx I X"
then have "âi. âfi αi. Fi i = (λr. (fi r, αi (fi r) r)) â§ fi â real_borel ââ©M count_space I â§ (âj. (j â range fi ⨠qbs_space (X j) â {}) ⶠαi j â qbs_Mx (X j))"
by(auto simp: coproduct_qbs_Mx_eq coprod_qbs_Mx'_def)
then obtain fi where
"âi. âαi. Fi i = (λr. (fi i r, αi (fi i r) r)) â§ fi i â real_borel ââ©M count_space I â§ (âj. (j â range (fi i) ⨠qbs_space (X j) â {}) ⶠαi j â qbs_Mx (X j))"
by(fastforce intro!: choice)
then obtain αi where
"âi. Fi i = (λr. (fi i r, αi i (fi i r) r)) â§ fi i â real_borel ââ©M count_space I â§ (âj. (j â range (fi i) ⨠qbs_space (X j) â {}) ⶠαi i j â qbs_Mx (X j))"
by(fastforce intro!: choice)
then have hf:
"âi. Fi i = (λr. (fi i r, αi i (fi i r) r))" "âi. fi i â real_borel ââ©M count_space I" "âi j. j â range (fi i) ⹠αi i j â qbs_Mx (X j)" "âi j. qbs_space (X j) â {} ⹠αi i j â qbs_Mx (X j)"
by auto
define f' where "f' ⡠(λr. fi (P r) r)"
define α' where "α' ⡠(λi r. αi (P r) i r)"
have 1:"(λr. Fi (P r) r) = (λr. (f' r, α' (f' r) r))"
by(simp add: α'_def f'_def hf)
have "f' â real_borel ââ©M count_space I"
proof -
note [measurable] = separate_measurable[OF h(1)]
have "(λ(n,r). fi n r) â count_space UNIV â¨â©M real_borel ââ©M count_space I"
by(auto intro!: measurable_pair_measure_countable1 simp: hf)
hence [measurable]:"(λ(n,r). fi n r) â nat_borel â¨â©M real_borel ââ©M count_space I"
using measurable_cong_sets[OF sets_pair_measure_cong[OF sets_borel_eq_count_space],of real_borel real_borel]
by auto
thus ?thesis
using measurable_comp[of "λr. (P r, r)" _ _ "(λ(n,r). fi n r)"]
by(simp add: f'_def)
qed
moreover have "âi. i â range f' ⹠α' i â qbs_Mx (X i)"
proof -
fix i
assume hi:"i â range f'"
then obtain r where hr:
"i = fi (P r) r" by(auto simp: f'_def)
hence "i â range (fi (P r))" by simp
hence "αi (P r) i â qbs_Mx (X i)" by(simp add: hf)
hence "qbs_space (X i) â {}"
by(auto simp: qbs_empty_equiv)
hence "âj. αi j i â qbs_Mx (X i)"
by(simp add: hf(4))
then show "α' i â qbs_Mx (X i)"
by(auto simp: α'_def h(1) intro!: qbs_closed3_dest[of P "λj. αi j i"])
qed
ultimately show "(λr. Fi (P r) r) â coprod_qbs_Mx I X"
by(auto intro!: coprod_qbs_MxI simp: 1)
qed
lemma coprod_qbs_correct: "Rep_quasi_borel (coprod_qbs I X) = (SIGMA i:I. qbs_space (X i), coprod_qbs_Mx I X)"
unfolding coprod_qbs_def
using is_quasi_borel_intro[OF coprod_qbs_f coprod_qbs_closed1 coprod_qbs_closed2 coprod_qbs_closed3]
by(fastforce intro!: Abs_quasi_borel_inverse)
lemma coproduct_qbs_space[simp]: "qbs_space (coprod_qbs I X) = (SIGMA i:I. qbs_space (X i))"
by(simp add: coprod_qbs_correct qbs_space_def)
lemma coproduct_qbs_Mx[simp]: "qbs_Mx (coprod_qbs I X) = coprod_qbs_Mx I X"
by(simp add: coprod_qbs_correct qbs_Mx_def)
lemma ini_morphism:
assumes "j â I"
shows "(λx. (j,x)) â X j ââ©Q (⨿â©Q iâI. X i)"
by(fastforce intro!: qbs_morphismI exI[where x="λr. j"] simp: coprod_qbs_Mx_def comp_def assms)
lemma coprod_qbs_canonical1:
assumes "countable I"
and "âi. i â I â¹ f i â X i ââ©Q Y"
shows "(λ(i,x). f i x) â (⨿â©Q i âI. X i) ââ©Q Y"
proof(rule qbs_morphismI)
fix α
assume "α â qbs_Mx (coprod_qbs I X)"
then obtain β g where ha:
"âi. i â range g ⹠β i â qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and hg[measurable]:"g â real_borel ââ©M count_space I"
by(fastforce simp: coprod_qbs_Mx_def)
define f' where "f' ⡠(λi r. f i (β i r))"
have "range g â I"
using measurable_space[OF hg] by auto
hence 1:"(âi. i â range g â¹ f' i â qbs_Mx Y)"
using qbs_morphismE(3)[OF assms(2) ha(1),simplified comp_def]
by(auto simp: f'_def)
have "(λ(i, x). f i x) â α = (λr. f' (g r) r)"
by(auto simp: ha(2) f'_def)
also have "... â qbs_Mx Y"
by(auto intro!: qbs_closed3_dest2'[OF assms(1) hg,of f',OF 1])
finally show "(λ(i, x). f i x) â α â qbs_Mx Y " .
qed
lemma coprod_qbs_canonical1':
assumes "countable I"
and "âi. i â I â¹ (λx. f (i,x)) â X i ââ©Q Y"
shows "f â (⨿â©Q i âI. X i) ââ©Q Y"
using coprod_qbs_canonical1[where f="curry f"] assms by(auto simp: curry_def)
text â¹ $\coprod_{i=0,1} X_i \cong X_1 + X_2$. âº
lemma coproduct_binary_coproduct:
"âf g. f â (⨿â©Q iâUNIV. if i then X else Y) ââ©Q X <+>â©Q Y â§ g â X <+>â©Q Y ââ©Q (⨿â©Q iâUNIV. if i then X else Y) â§
g â f = id â§ f â g = id"
proof(auto intro!: exI[where x="λ(b,z). if b then Inl z else Inr z"] exI[where x="case_sum (λz. (True,z)) (λz. (False,z))"])
show "(λ(b, z). if b then Inl z else Inr z) â (⨿â©Q iâUNIV. if i then X else Y) ââ©Q X <+>â©Q Y"
proof(rule qbs_morphismI)
fix α
assume " α â qbs_Mx (⨿â©Q iâUNIV. if i then X else Y)"
then obtain f β where hf:
"α = (λr. (f r, β (f r) r))" "f â real_borel ââ©M count_space UNIV" "âi. i â range f ⹠β i â qbs_Mx (if i then X else Y)"
by(auto simp: coprod_qbs_Mx_def)
consider "range f = {True}" | "range f = {False}" | "range f = {True,False}"
by auto
thus "(λ(b, z). if b then Inl z else Inr z) â α â qbs_Mx (X <+>â©Q Y)"
proof cases
case 1
then have "âr. f r = True"
by auto
then show ?thesis
using hf(3)
by(auto intro!: bexI[where x="{}"] bexI[where x="β True"] simp: copair_qbs_Mx_def split_beta' comp_def hf(1))
next
case 2
then have "âr. f r = False"
by auto
then show ?thesis
using hf(3)
by(auto intro!: bexI[where x="UNIV"] bexI[where x="β False"] simp: copair_qbs_Mx_def split_beta' comp_def hf(1))
next
case 3
then have 4:"f -` {True} â sets real_borel"
using measurable_sets[OF hf(2)] by simp
have 5:"f -` {True} â {} â§ f -` {True} â UNIV"
using 3
by (metis empty_iff imageE insertCI vimage_singleton_eq)
have 6:"β True â qbs_Mx X" "β False â qbs_Mx Y"
using hf(3)[of True] hf(3)[of False] by(auto simp: 3)
show ?thesis
apply(simp add: copair_qbs_Mx_def)
apply(intro bexI[OF _ 4])
apply(simp add: 5)
apply(intro bexI[OF _ 6(1)] bexI[OF _ 6(2)])
apply(auto simp add: hf(1) comp_def)
done
qed
qed
next
show "case_sum (Pair True) (Pair False) â X <+>â©Q Y ââ©Q (⨿â©Q iâUNIV. if i then X else Y)"
proof(rule qbs_morphismI)
fix α
assume "α â qbs_Mx (X <+>â©Q Y)"
then obtain S where hs:
"S â sets real_borel" "S = {} â¶ (â α1â qbs_Mx X. α = (λr. Inl (α1 r)))" "S = UNIV â¶ (â α2â qbs_Mx Y. α = (λr. Inr (α2 r)))"
"(S â {} â§ S â UNIV) â¶ (â α1â qbs_Mx X. â α2â qbs_Mx Y. α = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r))))"
by(auto simp: copair_qbs_Mx_def)
consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto
thus "case_sum (Pair True) (Pair False) â α â qbs_Mx (⨿â©Q iâUNIV. if i then X else Y)"
proof cases
case 1
then obtain α1 where ha:
"α1â qbs_Mx X" "α = (λr. Inl (α1 r))"
using hs(2) by auto
hence "case_sum (Pair True) (Pair False) â α = (λr. (True, α1 r))"
by auto
thus ?thesis
by(auto intro!: coprod_qbs_MxI simp: ha)
next
case 2
then obtain α2 where ha:
"α2â qbs_Mx Y" "α = (λr. Inr (α2 r))"
using hs(3) by auto
hence "case_sum (Pair True) (Pair False) â α = (λr. (False, α2 r))"
by auto
thus ?thesis
by(auto intro!: coprod_qbs_MxI simp: ha)
next
case 3
then obtain α1 α2 where ha:
"α1â qbs_Mx X" "α2â qbs_Mx Y" "α = (λr. (if (r â S) then Inl (α1 r) else Inr (α2 r)))"
using hs(4) by auto
define f :: "real â bool" where "f â¡ (λr. r â S)"
define α' where "α' ⡠(λi. if i then α1 else α2)"
have "case_sum (Pair True) (Pair False) â α = (λr. (f r, α' (f r) r))"
by(auto simp: f_def α'_def ha(3))
thus ?thesis
using hs(1)
by(auto intro!: coprod_qbs_MxI simp: ha α'_def f_def)
qed
qed
next
show "(λ(b, z). if b then Inl z else Inr z) â case_sum (Pair True) (Pair False) = id"
by (auto simp add: sum.case_eq_if )
qed
subsubsection â¹ Lists âº
abbreviation "list_of X ⡠⨿â©Q nâ(UNIV :: nat set). (Î â©Q iâ{..<n}. X)"
abbreviation list_nil :: "nat à (nat â 'a)" where
"list_nil ⡠(0, λn. undefined)"
abbreviation list_cons :: "['a, nat à (nat â 'a)] â nat à (nat â 'a)" where
"list_cons x l ⡠(Suc (fst l), (λn. if n = 0 then x else (snd l) (n - 1)))"
definition list_head :: "nat à (nat â 'a) â 'a" where
"list_head l = snd l 0"
definition list_tail :: "nat à (nat â 'a) â nat à (nat â 'a)" where
"list_tail l = (fst l - 1, λm. (snd l) (Suc m))"
lemma list_simp1:
"list_nil â list_cons x l"
by simp
lemma list_simp2:
assumes "list_cons a al = list_cons b bl"
shows "a = b" "al = bl"
proof -
have "a = snd (list_cons a al) 0"
"b = snd (list_cons b bl) 0"
by auto
thus "a = b"
by(simp add: assms)
next
have "fst al = fst bl"
using assms by simp
moreover have "snd al = snd bl"
proof
fix n
have "snd al n = snd (list_cons a al) (Suc n)"
by simp
also have "... = snd (list_cons b bl) (Suc n)"
by (simp add: assms)
also have "... = snd bl n"
by simp
finally show "snd al n = snd bl n" .
qed
ultimately show "al = bl"
by (simp add: prod.expand)
qed
lemma list_simp3:
shows "list_head (list_cons a l) = a"
by(simp add: list_head_def)
lemma list_simp4:
assumes "l â qbs_space (list_of X)"
shows "list_tail (list_cons a l) = l"
using assms by(simp_all add: list_tail_def)
lemma list_decomp1:
assumes "l â qbs_space (list_of X)"
shows "l = list_nil â¨
(âa l'. a â qbs_space X â§ l' â qbs_space (list_of X) â§ l = list_cons a l')"
proof(cases l)
case hl:(Pair n f)
show ?thesis
proof(cases n)
case 0
then show ?thesis
using assms hl by simp
next
case hn:(Suc n')
define f' where "f' ⡠λm. f (Suc m)"
have "l = list_cons (f 0) (n',f')"
proof(simp add: hl hn, standard)
fix m
show "f m = (if m = 0 then f 0 else snd (n', f') (m - 1))"
using assms hl by(cases m; fastforce simp: f'_def)
qed
moreover have "(n', f') â qbs_space (list_of X)"
proof(simp,rule PiE_I)
show "âx. x â {..<n'} â¹ f' x â qbs_space X"
using assms hl hn by(fastforce simp: f'_def)
next
fix x
assume 1:"x â {..<n'}"
thus " f' x = undefined"
using hl assms hn by(auto simp: f'_def)
qed
ultimately show ?thesis
using hl assms
by(auto intro!: exI[where x="f 0"] exI[where x="(n',λm. if m = 0 then undefined else f (Suc m))"])
qed
qed
lemma list_simp5:
assumes "l â qbs_space (list_of X)"
and "l â list_nil"
shows "l = list_cons (list_head l) (list_tail l)"
proof -
obtain a l' where hl:
"a â qbs_space X" "l' â qbs_space (list_of X)" "l = list_cons a l'"
using list_decomp1[OF assms(1)] assms(2) by blast
hence "list_head l = a" "list_tail l = l'"
using list_simp3 list_simp4 by auto
thus ?thesis
using hl(3) list_simp2 by auto
qed
lemma list_simp6:
"list_nil â qbs_space (list_of X)"
by simp
lemma list_simp7:
assumes "a â qbs_space X"
and "l â qbs_space (list_of X)"
shows "list_cons a l â qbs_space (list_of X)"
using assms by(fastforce simp: PiE_def extensional_def)
lemma list_destruct_rule:
assumes "l â qbs_space (list_of X)"
"P list_nil"
and "âa l'. a â qbs_space X â¹ l' â qbs_space (list_of X) â¹ P (list_cons a l')"
shows "P l"
by(rule disjE[OF list_decomp1[OF assms(1)]]) (use assms in auto)
lemma list_induct_rule:
assumes "l â qbs_space (list_of X)"
"P list_nil"
and "âa l'. a â qbs_space X â¹ l' â qbs_space (list_of X) â¹ P l' â¹ P (list_cons a l')"
shows "P l"
proof(cases l)
case hl:(Pair n f)
then show ?thesis
using assms(1)
proof(induction n arbitrary: f l)
case 0
then show ?case
using assms(1,2) by simp
next
case ih:(Suc n)
then obtain a l' where hl:
"a â qbs_space X" "l' â qbs_space (list_of X)" "l = list_cons a l'"
using list_decomp1 by blast
have "P l'"
using ih hl(3)
by(auto intro!: ih(1)[OF _ hl(2),of "snd l'"])
from assms(3)[OF hl(1,2) this]
show ?case
by(simp add: hl(3))
qed
qed
fun from_list :: "'a list â nat à (nat â 'a)" where
"from_list [] = list_nil" |
"from_list (a#l) = list_cons a (from_list l)"
fun to_list' :: "nat â (nat â 'a) â 'a list" where
"to_list' 0 _ = []" |
"to_list' (Suc n) f = f 0 # to_list' n (λn. f (Suc n))"
definition to_list :: "nat à (nat â 'a) â 'a list" where
"to_list â¡ case_prod to_list'"
lemma to_list_simp1:
shows "to_list list_nil = []"
by(simp add: to_list_def)
lemma to_list_simp2:
assumes "l â qbs_space (list_of X)"
shows "to_list (list_cons a l) = a # to_list l"
using assms by(auto simp:PiE_def to_list_def)
lemma from_list_length:
"fst (from_list l) = length l"
by(induction l, simp_all)
lemma from_list_in_list_of:
assumes "set l â qbs_space X"
shows "from_list l â qbs_space (list_of X)"
using assms by(induction l) (auto simp: PiE_def extensional_def Pi_def)
lemma from_list_in_list_of':
shows "from_list l â qbs_space (list_of (Abs_quasi_borel (UNIV,UNIV)))"
proof -
have "set l â qbs_space (Abs_quasi_borel (UNIV,UNIV))"
by(simp add: qbs_space_def Abs_quasi_borel_inverse[of "(UNIV,UNIV)",simplified is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def,simplified])
thus ?thesis
using from_list_in_list_of by blast
qed
lemma list_cons_in_list_of:
assumes "set (a#l) â qbs_space X"
shows "list_cons a (from_list l) â qbs_space (list_of X)"
using from_list_in_list_of[OF assms] by simp
lemma from_list_to_list_ident:
"(to_list â from_list) l = l"
by(induction l)
(simp add: to_list_def,simp add: to_list_simp2[OF from_list_in_list_of'])
lemma to_list_from_list_ident:
assumes "l â qbs_space (list_of X)"
shows "(from_list â to_list) l = l"
proof(rule list_induct_rule[OF assms])
fix a l'
assume h: "l' â qbs_space (list_of X)"
and ih:"(from_list â to_list) l' = l'"
show "(from_list â to_list) (list_cons a l') = list_cons a l'"
by(auto simp add: to_list_simp2[OF h] ih[simplified])
qed (simp add: to_list_simp1)
definition rec_list' :: "'b â ('a â (nat à (nat â 'a)) â 'b â 'b) â (nat à (nat â 'a)) â 'b" where
"rec_list' t0 f l ⡠(rec_list t0 (λx l'. f x (from_list l')) (to_list l))"
lemma rec_list'_simp1:
"rec_list' t f list_nil = t"
by(simp add: rec_list'_def to_list_simp1)
lemma rec_list'_simp2:
assumes "l â qbs_space (list_of X)"
shows "rec_list' t f (list_cons x l) = f x l (rec_list' t f l)"
by(simp add: rec_list'_def to_list_simp2[OF assms] to_list_from_list_ident[OF assms,simplified])
end>
Theory Exponent_QuasiBorel
subsection â¹Function Spacesâº
theory Exponent_QuasiBorel
imports "CoProduct_QuasiBorel"
begin
subsubsection â¹ Function Spaces âº
definition exp_qbs_Mx :: "['a quasi_borel, 'b quasi_borel] â (real â 'a => 'b) set" where
"exp_qbs_Mx X Y â¡ {g :: real â 'a â 'b. case_prod g â ââ©Q â¨â©Q X ââ©Q Y} "
definition exp_qbs :: "['a quasi_borel, 'b quasi_borel] â ('a â 'b) quasi_borel" (infixr "ââ©Q" 61) where
"X ââ©Q Y â¡ Abs_quasi_borel (X ââ©Q Y, exp_qbs_Mx X Y)"
lemma exp_qbs_f[simp]: "exp_qbs_Mx X Y â UNIV â (X :: 'a quasi_borel) ââ©Q (Y :: 'b quasi_borel)"
proof(auto intro!: qbs_morphismI)
fix f α r
assume h:"f â exp_qbs_Mx X Y"
"α â qbs_Mx X"
have "f r â α = (λy. case_prod f (r,y)) â α"
by auto
also have "... â qbs_Mx Y"
using qbs_morphism_Pair1'[of r "ââ©Q" "case_prod f" X Y] h
by(auto simp: exp_qbs_Mx_def)
finally show "f r â α â qbs_Mx Y" .
qed
lemma exp_qbs_closed1: "qbs_closed1 (exp_qbs_Mx X Y)"
proof(rule qbs_closed1I)
fix a
fix f
assume h:"a â exp_qbs_Mx X Y"
"f â real_borel ââ©M real_borel"
have "a â f = (λr y. case_prod a (f r,y))" by auto
moreover have "case_prod ... â ââ©Q â¨â©Q X ââ©Q Y"
proof -
have "case_prod (λr y. case_prod a (f r,y)) = case_prod a â map_prod f id"
by auto
also have "... â ââ©Q â¨â©Q X ââ©Q Y"
using h
by(auto intro!: qbs_morphism_comp qbs_morphism_map_prod simp: exp_qbs_Mx_def)
finally show ?thesis .
qed
ultimately show "a â f â exp_qbs_Mx X Y"
by (simp add: exp_qbs_Mx_def)
qed
lemma exp_qbs_closed2: "qbs_closed2 (X ââ©Q Y) (exp_qbs_Mx X Y)"
by(auto intro!: qbs_closed2I qbs_morphism_snd'' simp: exp_qbs_Mx_def split_beta')
lemma exp_qbs_closed3:"qbs_closed3 (exp_qbs_Mx X Y)"
proof(rule qbs_closed3I)
fix P :: "real â nat"
fix Fi :: "nat â real â _"
assume h:"âi. P -` {i} â sets real_borel"
"âi. Fi i â exp_qbs_Mx X Y"
show "(λr. Fi (P r) r) â exp_qbs_Mx X Y"
unfolding exp_qbs_Mx_def
proof(auto intro!: qbs_morphismI)
fix α β
assume h':"α â pair_qbs_Mx ââ©Q X "
have 1:"âi. (λ(r,x). Fi i r x) â α â qbs_Mx Y"
using qbs_morphismE(3)[OF h(2)[simplified exp_qbs_Mx_def,simplified]] h'
by(simp add: exp_qbs_Mx_def)
have 2:"âi. (P â (λr. fst (α r))) -` {i} â sets real_borel"
using separate_measurable[OF h(1)] h'
by(auto intro!: measurable_separate simp: pair_qbs_Mx_def comp_def)
show "(λ(r, y). Fi (P r) r y) â α â qbs_Mx Y"
using qbs_closed3_dest[OF 2,of "λi. (λ(r,x). Fi i r x) â α",OF 1]
by(simp add: comp_def split_beta')
qed
qed
lemma exp_qbs_correct: "Rep_quasi_borel (exp_qbs X Y) = (X ââ©Q Y, exp_qbs_Mx X Y)"
unfolding exp_qbs_def
by(auto intro!: Abs_quasi_borel_inverse exp_qbs_f simp: exp_qbs_closed1 exp_qbs_closed2 exp_qbs_closed3)
lemma exp_qbs_space[simp]: "qbs_space (exp_qbs X Y) = X ââ©Q Y"
by(simp add: qbs_space_def exp_qbs_correct)
lemma exp_qbs_Mx[simp]: "qbs_Mx (exp_qbs X Y) = exp_qbs_Mx X Y"
by(simp add: qbs_Mx_def exp_qbs_correct)
lemma qbs_exp_morphismI:
assumes "âα β. α â qbs_Mx X â¹
β â pair_qbs_Mx real_quasi_borel Y â¹
(λ(r,x). (f â α) r x) â β â qbs_Mx Z"
shows "f â X ââ©Q exp_qbs Y Z"
using assms
by(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def comp_def)
definition qbs_eval :: "(('a â 'b) Ã 'a) â 'b" where
"qbs_eval a â¡ (fst a) (snd a)"
lemma qbs_eval_morphism:
"qbs_eval â (exp_qbs X Y) â¨â©Q X ââ©Q Y"
proof(rule qbs_morphismI,simp)
fix f
assume "f â pair_qbs_Mx (exp_qbs X Y) X"
let ?f1 = "fst â f"
let ?f2 = "snd â f"
define g :: "real â real à _"
where "g ⡠λr.(r,?f2 r)"
have "g â qbs_Mx (real_quasi_borel â¨â©Q X)"
proof(auto simp add: pair_qbs_Mx_def)
have "fst â g = id" by(auto simp add: g_def comp_def)
thus "fst â g â real_borel ââ©M real_borel" by(auto simp add: measurable_ident)
next
have "snd â g = ?f2" by(auto simp add: g_def)
thus "snd â g â qbs_Mx X"
using â¹f â pair_qbs_Mx (exp_qbs X Y) X⺠pair_qbs_Mx_def by auto
qed
moreover have "?f1 â exp_qbs_Mx X Y"
using â¹f â pair_qbs_Mx (exp_qbs X Y) Xâº
by(simp add: pair_qbs_Mx_def)
ultimately have "(λ(r,x). (?f1 r x)) â g â qbs_Mx Y"
by (auto simp add: exp_qbs_Mx_def qbs_morphism_def)
(metis (mono_tags, lifting) case_prod_conv comp_apply cond_case_prod_eta)
moreover have "(λ(r,x). (?f1 r x)) â g = qbs_eval â f"
by(auto simp add: case_prod_unfold g_def qbs_eval_def)
ultimately show "qbs_eval â f â qbs_Mx Y" by simp
qed
lemma curry_morphism:
"curry â exp_qbs (X â¨â©Q Y) Z ââ©Q exp_qbs X (exp_qbs Y Z)"
proof(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def)
fix k α α'
assume h:"(λ(r, xy). k r xy) â ââ©Q â¨â©Q X â¨â©Q Y ââ©Q Z"
"α â pair_qbs_Mx ââ©Q X"
"α' â pair_qbs_Mx ââ©Q Y"
define β where
"β ⡠(λr. (fst (α (fst (α' r))),(snd (α (fst (α' r))), snd (α' r))))"
have "(λ(x, y). ((λ(x, y). (curry â k) x y) â α) x y) â α' = (λ(r, xy). k r xy) â β"
by(simp add: curry_def split_beta' comp_def β_def)
also have "... â qbs_Mx Z"
proof -
have "β â qbs_Mx (ââ©Q â¨â©Q X â¨â©Q Y)"
using h(2,3) qbs_closed1_dest[of _ _ "(λx. fst (α' x))"]
by(auto simp: pair_qbs_Mx_def β_def comp_def)
thus ?thesis
using h by auto
qed
finally show "(λ(x, y). ((λ(x, y). (curry â k) x y) â α) x y) â α' â qbs_Mx Z" .
qed
lemma curry_preserves_morphisms:
assumes "f â X â¨â©Q Y ââ©Q Z"
shows "curry f â X ââ©Q exp_qbs Y Z"
by(rule qbs_morphismE(2)[OF curry_morphism,simplified,OF assms])
lemma uncurry_morphism:
"case_prod â exp_qbs X (exp_qbs Y Z) ââ©Q exp_qbs (X â¨â©Q Y) Z"
proof(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def)
fix k α
assume h:"(λ(x, y). k x y) â ââ©Q â¨â©Q X ââ©Q exp_qbs Y Z"
"α â pair_qbs_Mx ââ©Q (X â¨â©Q Y)"
have "(λ(x, y). (case_prod â k) x y) â α = (λ(r,y). k (fst (α r)) (fst (snd (α r))) y) â (λr. (r,snd (snd (α r))))"
by(simp add: split_beta' comp_def)
also have "... â qbs_Mx Z"
proof(rule qbs_morphismE(3)[where X="ââ©Q â¨â©Q Y"])
have "(λr. k (fst (α r)) (fst (snd (α r)))) = (λ(x, y). k x y) â (λr. (fst (α r),fst (snd (α r))))"
by auto
also have "... â qbs_Mx (exp_qbs Y Z)"
apply(rule qbs_morphismE(3)[where X="ââ©Q â¨â©Q X"])
using h(2) by(auto simp: h(1) pair_qbs_Mx_def comp_def)
finally show " (λ(r, y). k (fst (α r)) (fst (snd (α r))) y) â ââ©Q â¨â©Q Y ââ©Q Z"
by(simp add: exp_qbs_Mx_def)
next
show "(λr. (r, snd (snd (α r)))) â qbs_Mx (ââ©Q â¨â©Q Y)"
using h(2) by(simp add: pair_qbs_Mx_def comp_def)
qed
finally show "(λ(x, y). (case_prod â k) x y) â α â qbs_Mx Z" .
qed
lemma uncurry_preserves_morphisms:
assumes "f â X ââ©Q exp_qbs Y Z"
shows "case_prod f â X â¨â©Q Y ââ©Q Z"
by(rule qbs_morphismE(2)[OF uncurry_morphism,simplified,OF assms])
lemma arg_swap_morphism:
assumes "f â X ââ©Q exp_qbs Y Z"
shows "(λy x. f x y) â Y ââ©Q exp_qbs X Z"
using curry_preserves_morphisms[OF qbs_morphism_pair_swap[OF uncurry_preserves_morphisms[OF assms]]]
by simp
lemma exp_qbs_comp_morphism:
assumes "f â W ââ©Q exp_qbs X Y"
and "g â W ââ©Q exp_qbs Y Z"
shows "(λw. g w â f w) â W ââ©Q exp_qbs X Z"
proof(rule qbs_exp_morphismI)
fix α β
assume h: "α â qbs_Mx W"
"β â pair_qbs_Mx ââ©Q X"
have "(λ(r, x). ((λw. g w â f w) â α) r x) â β= case_prod g â (λr. ((α â (fst â β)) r, case_prod f ((α â (fst â β)) r, (snd â β) r)))"
by(simp add: split_beta' comp_def)
also have "... â qbs_Mx Z"
proof -
have "(λr. ((α â (fst â β)) r, case_prod f ((α â (fst â β)) r, (snd â β) r))) â qbs_Mx (W â¨â©Q Y)"
proof(auto simp add: pair_qbs_Mx_def)
have "fst â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) = α â (fst â β)"
by (simp add: comp_def)
also have "... â qbs_Mx W"
using qbs_decomp[of W] h
by(simp add: pair_qbs_Mx_def qbs_closed1_def)
finally show "fst â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) â qbs_Mx W" .
next
have [simp]:"snd â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) = case_prod f â (λr. ((α â (fst â β)) r, (snd â β) r))"
by(simp add: comp_def)
have "(λr. ((α â (fst â β)) r, (snd â β) r)) â qbs_Mx (W â¨â©Q X)"
proof(auto simp add: pair_qbs_Mx_def)
have "fst â (λr. (α (fst (β r)), snd (β r)))= α â (fst â β)"
by (simp add: comp_def)
also have "... â qbs_Mx W"
using qbs_decomp[of W] h
by(simp add: pair_qbs_Mx_def qbs_closed1_def)
finally show "fst â (λr. (α (fst (β r)), snd (β r))) â qbs_Mx W" .
next
show "snd â (λr. (α (fst (β r)), snd (β r))) â qbs_Mx X"
using h
by(simp add: pair_qbs_Mx_def comp_def)
qed
hence "case_prod f â (λr. ((α â (fst â β)) r, (snd â β) r)) â qbs_Mx Y"
using uncurry_preserves_morphisms[OF assms(1)] by auto
thus "snd â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) â qbs_Mx Y"
by simp
qed
thus ?thesis
using uncurry_preserves_morphisms[OF assms(2)]
by auto
qed
finally show "(λ(r, x). ((λw. g w â f w) â α) r x) â β â qbs_Mx Z" .
qed
lemma case_sum_morphism:
"case_prod case_sum â exp_qbs X Z â¨â©Q exp_qbs Y Z ââ©Q exp_qbs (X <+>â©Q Y) Z"
proof(rule qbs_exp_morphismI)
fix α β
assume h0:"α â qbs_Mx (exp_qbs X Z â¨â©Q exp_qbs Y Z)"
"β â pair_qbs_Mx ââ©Q (X <+>â©Q Y)"
let ?α1 = "fst â α"
let ?α2 = "snd â α"
let ?β1 = "fst â β"
let ?β2 = "snd â β"
have h:"?α1 â exp_qbs_Mx X Z"
"?α2 â exp_qbs_Mx Y Z"
"?β1 â real_borel ââ©M real_borel"
"?β2 â copair_qbs_Mx X Y"
using h0 by (auto simp add: pair_qbs_Mx_def)
hence "âSâsets real_borel. (S = {} â¶ (âα1âqbs_Mx X. ?β2 = (λr. Inl (α1 r)))) â§
(S = UNIV â¶ (âα2âqbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) â§
(S â {} â§ S â UNIV â¶
(âα1âqbs_Mx X. âα2âqbs_Mx Y. ?β2 = (λr. if r â S then Inl (α1 r) else Inr (α2 r))))"
by(simp add: copair_qbs_Mx_def)
then obtain S :: "real set" where hs:
"Sâsets real_borel â§ (S = {} â¶ (âα1âqbs_Mx X. ?β2 = (λr. Inl (α1 r)))) â§
(S = UNIV â¶ (âα2âqbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) â§
(S â {} â§ S â UNIV â¶
(âα1âqbs_Mx X. âα2âqbs_Mx Y. ?β2 = (λr. if r â S then Inl (α1 r) else Inr (α2 r))))"
by auto
show "(λ(r, x). ((λ(x, y). case_sum x y) â α) r x) â β â qbs_Mx Z"
proof -
have "(λ(r, x). ((λ(x, y). case_sum x y) â α) r x) â β = (λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r))"
(is "?lhs = ?rhs")
by(auto simp: split_beta' comp_def) (metis comp_apply)
also have "... â qbs_Mx Z"
(is "?f â _")
proof -
consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto
then show ?thesis
proof cases
case 1
then obtain α1 where h1:
"α1âqbs_Mx X â§ ?β2 = (λr. Inl (α1 r))"
using hs by auto
then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) = (λr. ?α1 (?β1 r) (α1 r))"
by simp
also have "... = case_prod ?α1 â (λr. (?β1 r,α1 r))"
by auto
also have "... â ââ©Q ââ©Q Z"
apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q X"])
apply(rule qbs_morphism_tuple)
using h(3)
apply blast
using qbs_Mx_is_morphisms h1
apply blast
using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q X"] h(1)
by (simp add: exp_qbs_Mx_def)
finally show ?thesis
using qbs_Mx_is_morphisms by auto
next
case 2
then obtain α2 where h2:
"α2âqbs_Mx Y â§ ?β2 = (λr. Inr (α2 r))"
using hs by auto
then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) = (λr. ?α2 (?β1 r) (α2 r))"
by simp
also have "... = case_prod ?α2 â (λr. (?β1 r,α2 r))"
by auto
also have "... â ââ©Q ââ©Q Z"
apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q Y"])
apply(rule qbs_morphism_tuple)
using h(3)
apply blast
using qbs_Mx_is_morphisms h2
apply blast
using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q Y"] h(2)
by (simp add: exp_qbs_Mx_def)
finally show ?thesis
using qbs_Mx_is_morphisms by auto
next
case 3
then obtain α1 α2 where h3:
"α1âqbs_Mx X ⧠α2âqbs_Mx Y â§ ?β2 = (λr. if r â S then Inl (α1 r) else Inr (α2 r))"
using hs by auto
define P :: "real â nat"
where "P â¡ (λr. if r â S then 0 else 1)"
define γ :: "nat â real â _"
where "γ ⡠(λn r. if n = 0 then ?α1 (?β1 r) (α1 r) else ?α2 (?β1 r) (α2 r))"
then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) =(λr. γ (P r) r)"
by(auto simp add: P_def γ_def h3)
also have "... â qbs_Mx Z"
proof -
have "âi. P -` {i} â sets real_borel"
using hs borel_comp[of S] by(simp add: P_def)
moreover have"âi. γ i â qbs_Mx Z"
proof
fix i :: nat
consider "i = 0" | "i â 0" by auto
then show "γ i â qbs_Mx Z"
proof cases
case 1
then have "γ i = (λr. ?α1 (?β1 r) (α1 r))"
by(simp add: γ_def)
also have "... = case_prod ?α1 â (λr. (?β1 r,α1 r))"
by auto
also have "... â ââ©Q ââ©Q Z"
apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q X"])
apply(rule qbs_morphism_tuple)
using h(3)
apply blast
using qbs_Mx_is_morphisms h3
apply blast
using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q X"] h(1)
by (simp add: exp_qbs_Mx_def)
finally show ?thesis
using qbs_Mx_is_morphisms by auto
next
case 2
then have "γ i = (λr. ?α2 (?β1 r) (α2 r))"
by(simp add: γ_def)
also have "... = case_prod ?α2 â (λr. (?β1 r,α2 r))"
by auto
also have "... â ââ©Q ââ©Q Z"
apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q Y"])
apply(rule qbs_morphism_tuple)
using h(3)
apply blast
using qbs_Mx_is_morphisms h3
apply blast
using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q Y"] h(2)
by (simp add: exp_qbs_Mx_def)
finally show ?thesis
using qbs_Mx_is_morphisms by auto
qed
qed
ultimately show ?thesis
using qbs_decomp[of Z]
by(simp add: qbs_closed3_def)
qed
finally show ?thesis .
qed
qed
finally show ?thesis .
qed
qed
lemma not_qbs_morphism:
"Not â ð¹â©Q ââ©Q ð¹â©Q"
by(auto intro!: bool_qbs_morphism)
lemma or_qbs_morphism:
"(â¨) â ð¹â©Q ââ©Q exp_qbs ð¹â©Q ð¹â©Q"
by(auto intro!: bool_qbs_morphism)
lemma and_qbs_morphism:
"(â§) â ð¹â©Q ââ©Q exp_qbs ð¹â©Q ð¹â©Q"
by(auto intro!: bool_qbs_morphism)
lemma implies_qbs_morphism:
"(â¶) â ð¹â©Q ââ©Q ð¹â©Q ââ©Q ð¹â©Q"
by(auto intro!: bool_qbs_morphism)
lemma less_nat_qbs_morphism:
"(<) â ââ©Q ââ©Q exp_qbs ââ©Q ð¹â©Q"
by(auto intro!: nat_qbs_morphism)
lemma less_real_qbs_morphism:
"(<) â ââ©Q ââ©Q exp_qbs ââ©Q ð¹â©Q"
proof(rule curry_preserves_morphisms[where f="(λ(z :: real à real). fst z < snd z)",simplified curry_def,simplified])
have "(λz. fst z < snd z) â real_borel â¨â©M real_borel ââ©M bool_borel"
using borel_measurable_pred_less[OF measurable_fst measurable_snd,simplified measurable_cong_sets[OF refl sets_borel_eq_count_space[symmetric],of "borel â¨â©M borel"]]
by simp
thus "(λz. fst z < snd z) â ââ©Q â¨â©Q ââ©Q ââ©Q ð¹â©Q"
by auto
qed
lemma rec_list_morphism':
"rec_list' â qbs_space (exp_qbs Y (exp_qbs (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) (exp_qbs (list_of X) Y)))"
apply(simp,rule curry_preserves_morphisms[where f="λyf. rec_list' (fst yf) (snd yf)",simplified curry_def, simplified])
apply(rule arg_swap_morphism)
proof(rule coprod_qbs_canonical1')
fix n
show "(λx y. rec_list' (fst y) (snd y) (n, x)) â (Î â©Q iâ{..<n}. X) ââ©Q exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y"
proof(induction n)
case 0
show ?case
proof(rule curry_preserves_morphisms[of " (λ(x,y). rec_list' (fst y) (snd y) (0, x))", simplified],rule qbs_morphismI)
fix α
assume h:"α â qbs_Mx ((Î â©Q iâ{..<0::nat}. X) â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)))"
have "âr. fst (α r) = (λn. undefined)"
proof -
fix r
have "âi. (λr. fst (α r) i) = (λr. undefined)"
using h by(auto simp: exp_qbs_Mx_def prod_qbs_Mx_def pair_qbs_Mx_def comp_def split_beta')
thus "fst (α r) = (λn. undefined)"
by(fastforce dest: fun_cong)
qed
hence "(λ(x, y). rec_list' (fst y) (snd y) (0, x)) â α = (λx. fst (snd (α x)))"
by(auto simp: rec_list'_simp1 comp_def split_beta')
also have "... â qbs_Mx Y"
using h by(auto simp: pair_qbs_Mx_def comp_def)
finally show "(λ(x, y). rec_list' (fst y) (snd y) (0, x)) â α â qbs_Mx Y" .
qed
next
case ih:(Suc n)
show ?case
proof(rule qbs_morphismI)
fix α
assume h:"α â qbs_Mx (Î â©Q iâ{..<Suc n}. X)"
define α' where "α' ⡠(λr. snd (list_tail (Suc n, α r)))"
define a where "a ⡠(λr. α r 0)"
then have ha:"a â qbs_Mx X"
using h by(auto simp: prod_qbs_Mx_def)
have 1:"α' â qbs_Mx (Î â©Q iâ{..<n}. X)"
using h by(fastforce simp: prod_qbs_Mx_def list_tail_def α'_def)
hence 2: "âr. (n, α' r) â qbs_space (list_of X)"
using qbs_Mx_to_X[of α'] by fastforce
have 3: "âr. (Suc n, α r) â qbs_space (list_of X)"
using qbs_Mx_to_X[of α] h by fastforce
have 4: "âr. (n, α' r) = list_tail (Suc n, α r)"
by(simp add: list_tail_def α'_def)
have 5: "âr. (Suc n, α r) = list_cons (a r) (n, α' r)"
unfolding a_def by(simp add: list_simp5[OF 3,simplified 4[symmetric],simplified list_head_def]) auto
have 6: "(λr. (n, α' r)) â qbs_Mx (list_of X)"
using 1 by(auto intro!: coprod_qbs_MxI)
have "(λx y. rec_list' (fst y) (snd y) (Suc n, x)) â α = (λr y. rec_list' (fst y) (snd y) (Suc n, α r))"
by auto
also have "... = (λr y. snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r)))"
by(simp only: 5 rec_list'_simp2[OF 2])
also have "... â qbs_Mx (exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y)"
proof -
have "(λ(r,y). snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r))) = (λ(y,x1,x2,x3). y x1 x2 x3) â (λ(r,y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r)))"
by auto
also have "... â ââ©Q â¨â©Q (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) ââ©Q Y"
proof(rule qbs_morphism_comp[where Y="exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y"])
show "(λ(r, y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r))) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y"
proof(auto simp: split_beta' intro!: qbs_morphism_tuple[OF qbs_morphism_snd''[OF snd_qbs_morphism] qbs_morphism_tuple[of "λ(r, y). a r" "ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))" X], OF _ qbs_morphism_tuple[of "λ(r,y). (n, α' r)"],of "list_of X" "λ(r,y). rec_list' (fst y) (snd y) (n, α' r)",simplified split_beta'])
show "(λx. a (fst x)) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q X"
using ha qbs_Mx_is_morphisms[of X] qbs_morphism_fst''[of a "ââ©Q" X] by auto
next
show "(λx. (n, α' (fst x))) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q list_of X"
using qbs_morphism_fst''[of "λr. (n, α' r)" "ââ©Q" "list_of X"] qbs_Mx_is_morphisms[of "list_of X"] 6 by auto
next
show "(λx. rec_list' (fst (snd x)) (snd (snd x)) (n, α' (fst x))) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q Y"
using qbs_morphismE(3)[OF ih 1, simplified comp_def] uncurry_preserves_morphisms[of "(λx y. rec_list' (fst y) (snd y) (n, α' x))" "ââ©Q" "Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))" Y] qbs_Mx_is_morphisms[of "exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y"]
by(fastforce simp: split_beta')
qed
next
show "(λ(y, x1, x2, x3). y x1 x2 x3) â exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y ââ©Q Y"
proof(rule qbs_morphismI)
fix β
assume "β â qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y)"
then have "â β1 β2 β3 β4. β = (λr. (β1 r, β2 r, β3 r, β4 r)) ⧠β1 â qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) ⧠β2 â qbs_Mx X ⧠β3 â qbs_Mx (list_of X) ⧠β4 â qbs_Mx Y"
by(auto intro!: exI[where x="fst â β"] exI[where x="fst â snd â β"] exI[where x="fst â snd â snd â β"] exI[where x="snd â snd â snd â β"] simp:pair_qbs_Mx_def comp_def)
then obtain β1 β2 β3 β4 where hb:
"β = (λr. (β1 r, β2 r, β3 r, β4 r))" "β1 â qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)))" "β2 â qbs_Mx X" "β3 â qbs_Mx (list_of X)" "β4 â qbs_Mx Y"
by auto
hence hbq:"(λ(((r,x1),x2),x3). β1 r x1 x2 x3) â ((ââ©Q â¨â©Q X) â¨â©Q list_of X) â¨â©Q Y ââ©Q Y"
by(simp add: exp_qbs_Mx_def) (meson uncurry_preserves_morphisms)
have "(λ(y, x1, x2, x3). y x1 x2 x3) â β = (λ(((r,x1),x2),x3). β1 r x1 x2 x3) â (λr. (((r,β2 r), β3 r), β4 r))"
by(auto simp: hb(1))
also have "... â ââ©Q ââ©Q Y"
using hb(2-5)
by(auto intro!: qbs_morphism_comp[OF qbs_morphism_tuple[OF qbs_morphism_tuple[OF qbs_morphism_tuple[OF qbs_morphism_ident']]] hbq] simp: qbs_Mx_is_morphisms)
finally show "(λ(y, x1, x2, x3). y x1 x2 x3) â β â qbs_Mx Y"
by(simp add: qbs_Mx_is_morphisms)
qed
qed
finally show ?thesis
by(simp add: exp_qbs_Mx_def)
qed
finally show "(λx y. rec_list' (fst y) (snd y) (Suc n, x)) â α â qbs_Mx (exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y)" .
qed
qed
qed simp
ende>
Theory Probability_Space_QuasiBorel
section â¹Probability Spacesâº
subsection â¹Probability Measures âº
theory Probability_Space_QuasiBorel
imports Exponent_QuasiBorel
begin
subsubsection â¹ Probability Measures âº
type_synonym 'a qbs_prob_t = "'a quasi_borel * (real â 'a) * real measure"
locale in_Mx =
fixes X :: "'a quasi_borel"
and α :: "real â 'a"
assumes in_Mx[simp]:"α â qbs_Mx X"
locale qbs_prob = in_Mx X α + real_distribution μ
for X :: "'a quasi_borel" and α and μ
begin
declare prob_space_axioms[simp]
lemma m_in_space_prob_algebra[simp]:
"μ â space (prob_algebra real_borel)"
using space_prob_algebra[of real_borel] by simp
end
locale pair_qbs_probs = qp1:qbs_prob X α μ + qp2:qbs_prob Y β ν
for X :: "'a quasi_borel"and α μ and Y :: "'b quasi_borel" and β ν
begin
sublocale pair_prob_space μ ν
by standard
lemma ab_measurable[measurable]:
"map_prod α β â real_borel â¨â©M real_borel ââ©M qbs_to_measure (X â¨â©Q Y)"
using qbs_morphism_map_prod[of α "ââ©Q" X β "ââ©Q" Y] qp1.in_Mx qp2.in_Mx l_preserves_morphisms[of "ââ©Q â¨â©Q ââ©Q" "X â¨â©Q Y"]
by(auto simp: qbs_Mx_is_morphisms)
lemma ab_g_in_Mx[simp]:
"map_prod α β â real_real.g â pair_qbs_Mx X Y"
using qbs_closed1_dest[OF qp1.in_Mx] qbs_closed1_dest[OF qp2.in_Mx]
by(auto simp add: pair_qbs_Mx_def comp_def)
sublocale qbs_prob "X â¨â©Q Y" "map_prod α β â real_real.g" "distr (μ â¨â©M ν) real_borel real_real.f"
by(auto simp: qbs_prob_def in_Mx_def)
end
locale pair_qbs_prob = qp1:qbs_prob X α μ + qp2:qbs_prob Y β ν
for X :: "'a quasi_borel"and α μ and Y :: "'a quasi_borel" and β ν
begin
sublocale pair_qbs_probs
by standard
lemma same_spaces[simp]:
assumes "Y = X"
shows "β â qbs_Mx X"
by(simp add: assms[symmetric])
end
lemma prob_algebra_real_prob_measure:
"p â space (prob_algebra (real_borel)) = real_distribution p"
proof
assume "p â space (prob_algebra real_borel)"
then show "real_distribution p"
unfolding real_distribution_def real_distribution_axioms_def
by(simp add: space_prob_algebra sets_eq_imp_space_eq)
next
assume "real_distribution p"
then interpret rd: real_distribution p .
show "p â space (prob_algebra real_borel)"
by (simp add: space_prob_algebra rd.prob_space_axioms)
qed
lemma qbs_probI:
assumes "α â qbs_Mx X"
and "sets μ = sets borel"
and "prob_space μ"
shows "qbs_prob X α μ"
using assms
by(auto intro!: qbs_prob.intro simp: in_Mx_def real_distribution_def real_distribution_axioms_def)
lemma qbs_empty_not_qbs_prob :"¬ qbs_prob (empty_quasi_borel) f M"
by(simp add: qbs_prob_def in_Mx_def)
definition qbs_prob_eq :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where
"qbs_prob_eq p1 p2 â¡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§
distr m1 (qbs_to_measure qbs1) a1 = distr m2 (qbs_to_measure qbs2) a2)"
definition qbs_prob_eq2 :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where
"qbs_prob_eq2 p1 p2 â¡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§
(âf â qbs1 ââ©Q real_quasi_borel.
(â«x. f (a1 x) â m1) = (â«x. f (a2 x) â m2)))"
definition qbs_prob_eq3 :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where
"qbs_prob_eq3 p1 p2 â¡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
(qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§
(âf â qbs1 ââ©Q real_quasi_borel.
(â k â qbs_space qbs1. 0 ⤠f k) â¶
(â«x. f (a1 x) â m1) = (â«x. f (a2 x) â m2))))"
definition qbs_prob_eq4 :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where
"qbs_prob_eq4 p1 p2 â¡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
(qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§
(âf â qbs1 ââ©Q ââ©Qâ©â¥â©0.
(â«â§+x. f (a1 x) â m1) = (â«â§+x. f (a2 x) â m2))))"
lemma(in qbs_prob) qbs_prob_eq_refl[simp]:
"qbs_prob_eq (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq_def qbs_prob_axioms)
lemma(in qbs_prob) qbs_prob_eq2_refl[simp]:
"qbs_prob_eq2 (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq2_def qbs_prob_axioms)
lemma(in qbs_prob) qbs_prob_eq3_refl[simp]:
"qbs_prob_eq3 (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq3_def qbs_prob_axioms)
lemma(in qbs_prob) qbs_prob_eq4_refl[simp]:
"qbs_prob_eq4 (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq4_def qbs_prob_axioms)
lemma(in pair_qbs_prob) qbs_prob_eq_intro:
assumes "X = Y"
and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
shows "qbs_prob_eq (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq_def)
lemma(in pair_qbs_prob) qbs_prob_eq2_intro:
assumes "X = Y"
and "âf. f â qbs_to_measure X ââ©M real_borel
â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)"
shows "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq2_def)
lemma(in pair_qbs_prob) qbs_prob_eq3_intro:
assumes "X = Y"
and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (â k â qbs_space X. 0 ⤠f k)
â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)"
shows "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq3_def)
lemma(in pair_qbs_prob) qbs_prob_eq4_intro:
assumes "X = Y"
and "âf. f â qbs_to_measure X ââ©M ennreal_borel
â¹ (â«â§+x. f (α x) â μ) = (â«â§+x. f (β x) â ν)"
shows "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq4_def)
lemma qbs_prob_eq_dest:
assumes "qbs_prob_eq (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
using assms by(auto simp: qbs_prob_eq_def)
lemma qbs_prob_eq2_dest:
assumes "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "âf. f â qbs_to_measure X ââ©M real_borel
â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)"
using assms by(auto simp: qbs_prob_eq2_def)
lemma qbs_prob_eq3_dest:
assumes "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (â k â qbs_space X. 0 ⤠f k)
â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)"
using assms by(auto simp: qbs_prob_eq3_def)
lemma qbs_prob_eq4_dest:
assumes "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "âf. f â qbs_to_measure X ââ©M ennreal_borel
â¹ (â«â§+x. f (α x) â μ) = (â«â§+x. f (β x) â ν)"
using assms by(auto simp: qbs_prob_eq4_def)
definition qbs_prob_t_ennintegral :: "['a qbs_prob_t, 'a â ennreal] â ennreal" where
"qbs_prob_t_ennintegral p f â¡
(if f â (fst p) ââ©Q ennreal_quasi_borel
then (â«â§+x. f (fst (snd p) x) â (snd (snd p))) else 0)"
definition qbs_prob_t_integral :: "['a qbs_prob_t, 'a â real] â real" where
"qbs_prob_t_integral p f â¡
(if f â (fst p) ââ©Q ââ©Q
then (â«x. f (fst (snd p) x) â (snd (snd p)))
else 0)"
definition qbs_prob_t_integrable :: "['a qbs_prob_t, 'a â real] â bool" where
"qbs_prob_t_integrable p f â¡ f â fst p ââ©Q real_quasi_borel â§ integrable (snd (snd p)) (f â (fst (snd p)))"
definition qbs_prob_t_measure :: "'a qbs_prob_t â 'a measure" where
"qbs_prob_t_measure p â¡ distr (snd (snd p)) (qbs_to_measure (fst p)) (fst (snd p))"
lemma qbs_prob_eq_symp:
"symp qbs_prob_eq"
by(simp add: symp_def qbs_prob_eq_def)
lemma qbs_prob_eq_transp:
"transp qbs_prob_eq"
by(simp add: transp_def qbs_prob_eq_def)
quotient_type 'a qbs_prob_space = "'a qbs_prob_t" / partial: qbs_prob_eq
morphisms rep_qbs_prob_space qbs_prob_space
proof(rule part_equivpI)
let ?U = "UNIV :: 'a set"
let ?Uf = "UNIV :: (real â 'a) set"
let ?f = "(λ_. undefined) :: real â 'a"
have "qbs_prob (Abs_quasi_borel (?U,?Uf)) ?f (return borel 0)"
proof(auto simp add: qbs_prob_def in_Mx_def)
have "Rep_quasi_borel (Abs_quasi_borel (?U,?Uf)) = (?U, ?Uf)"
using Abs_quasi_borel_inverse
by (auto simp add: qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
thus "(λ_. undefined) â qbs_Mx (Abs_quasi_borel (?U, ?Uf))"
by(simp add: qbs_Mx_def)
next
show "real_distribution (return borel 0)"
by (simp add: prob_space_return real_distribution_axioms_def real_distribution_def)
qed
thus "âx :: 'a qbs_prob_t . qbs_prob_eq x x"
unfolding qbs_prob_eq_def
by(auto intro!: exI[where x="(Abs_quasi_borel (?U,?Uf), ?f, return borel 0)"])
qed (simp_all add: qbs_prob_eq_symp qbs_prob_eq_transp)
interpretation qbs_prob_space : quot_type "qbs_prob_eq" "Abs_qbs_prob_space" "Rep_qbs_prob_space"
using Abs_qbs_prob_space_inverse Rep_qbs_prob_space
by(simp add: quot_type_def equivp_implies_part_equivp qbs_prob_space_equivp Rep_qbs_prob_space_inverse Rep_qbs_prob_space_inject) blast
lemma qbs_prob_space_induct:
assumes "âX α μ. qbs_prob X α μ â¹ P (qbs_prob_space (X,α,μ))"
shows "P s"
apply(rule qbs_prob_space.abs_induct)
using assms by(auto simp: qbs_prob_eq_def)
lemma qbs_prob_space_induct':
assumes "âX α μ. qbs_prob X α μ â¹ s = qbs_prob_space (X,α,μ)â¹ P (qbs_prob_space (X,α,μ))"
shows "P s"
by (metis (no_types, lifting) Rep_qbs_prob_space_inverse assms case_prodE qbs_prob_eq_def qbs_prob_space.abs_def qbs_prob_space.rep_prop qbs_prob_space_def)
lemma rep_qbs_prob_space:
"âX α μ. p = qbs_prob_space (X, α, μ) â§ qbs_prob X α μ"
by(rule qbs_prob_space.abs_induct,auto simp add: qbs_prob_eq_def)
lemma(in qbs_prob) in_Rep:
"(X, α, μ) â Rep_qbs_prob_space (qbs_prob_space (X,α,μ))"
by (metis mem_Collect_eq qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def)
lemma(in qbs_prob) if_in_Rep:
assumes "(X',α',μ') â Rep_qbs_prob_space (qbs_prob_space (X,α,μ))"
shows "X' = X"
"qbs_prob X' α' μ'"
"qbs_prob_eq (X,α,μ) (X',α',μ')"
proof -
have h:"X' = X"
by (metis assms mem_Collect_eq qbs_prob_eq_dest(3) qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def)
have [simp]:"qbs_prob X' α' μ'"
by (metis assms mem_Collect_eq prod_cases3 qbs_prob_eq_dest(2) qbs_prob_space.rep_prop)
have [simp]:"qbs_prob_eq (X,α,μ) (X',α',μ')"
by (metis assms mem_Collect_eq qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def)
show "X' = X"
"qbs_prob X' α' μ'"
"qbs_prob_eq (X,α,μ) (X',α',μ')"
by simp_all (simp add: h)
qed
lemma(in qbs_prob) in_Rep_induct:
assumes "âY β ν. (Y,β,ν) â Rep_qbs_prob_space (qbs_prob_space (X,α,μ)) â¹ P (Y,β,ν)"
shows "P (rep_qbs_prob_space (qbs_prob_space (X,α,μ)))"
unfolding rep_qbs_prob_space_def qbs_prob_space.rep_def
by(rule someI2[where a="(X,α,μ)"]) (use in_Rep assms in auto)
lemma qbs_prob_eq_2_implies_3 :
assumes "qbs_prob_eq2 p1 p2"
shows "qbs_prob_eq3 p1 p2"
using assms by(auto simp: qbs_prob_eq2_def qbs_prob_eq3_def)
lemma qbs_prob_eq_3_implies_1 :
assumes "qbs_prob_eq3 (p1 :: 'a qbs_prob_t) p2"
shows "qbs_prob_eq p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq3_def)
note [simp] = qbs_prob_eq3_dest(3)[OF h]
show "qbs_prob_eq (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq_intro)
show "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
proof(rule measure_eqI)
fix U
assume hu:"U â sets (distr μ (qbs_to_measure X) α)"
have "measure (distr μ (qbs_to_measure X) α) U = measure (distr ν (qbs_to_measure X) β) U"
(is "?lhs = ?rhs")
proof -
have "?lhs = measure μ (α -` U ⩠space μ)"
by(rule measure_distr) (use hu in simp_all)
also have "... = integralâ§L μ (indicat_real (α -` U))"
by simp
also have "... = (â«x. indicat_real U (α x) âμ)"
using indicator_vimage[of α U] Bochner_Integration.integral_cong[of μ _ "indicat_real (α -` U)" "λx. indicat_real U (α x)"]
by auto
also have "... = (â«x. indicat_real U (β x) âν)"
using qbs_prob_eq3_dest(4)[OF h,of "indicat_real U"] hu
by simp
also have "... = integralâ§L ν (indicat_real (β -` U))"
using indicator_vimage[of β U,symmetric] Bochner_Integration.integral_cong[of ν _ "λx. indicat_real U (β x)" "indicat_real (β -` U)"]
by blast
also have "... = measure ν (β -` U ⩠space ν)"
by simp
also have "... = ?rhs"
by(rule measure_distr[symmetric]) (use hu in simp_all)
finally show ?thesis .
qed
thus "emeasure (distr μ (qbs_to_measure X) α) U = emeasure (distr ν (qbs_to_measure X) β) U"
using qp.qp2.finite_measure_distr[of β] qp.qp1.finite_measure_distr[of α]
by(simp add: finite_measure.emeasure_eq_measure)
qed simp
qed simp
qed
lemma qbs_prob_eq_1_implies_2 :
assumes "qbs_prob_eq p1 (p2 :: 'a qbs_prob_t)"
shows "qbs_prob_eq2 p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq_def)
note [simp] = qbs_prob_eq_dest(3)[OF h]
show "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq2_intro)
fix f :: "'a â real"
assume [measurable]:"f â borel_measurable (qbs_to_measure X)"
show "(â«r. f (α r) â μ) = (â«r. f (β r) â ν)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (â«x. f x â(distr μ (qbs_to_measure X) α))"
by(simp add: Bochner_Integration.integral_distr[symmetric])
also have "... = (â«x. f x â(distr ν (qbs_to_measure X) β))"
by(simp add: qbs_prob_eq_dest(4)[OF h])
also have "... = ?rhs"
by(simp add: Bochner_Integration.integral_distr)
finally show ?thesis .
qed
qed simp
qed
lemma qbs_prob_eq_1_implies_4 :
assumes "qbs_prob_eq p1 p2"
shows "qbs_prob_eq4 p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq_def)
note [simp] = qbs_prob_eq_dest(3)[OF h]
show "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq4_intro)
fix f ::"'a â ennreal"
assume [measurable]:"f â borel_measurable (qbs_to_measure X)"
show "(â«â§+ x. f (α x) âμ) = (â«â§+ x. f (β x) âν)"
(is "?lhs = ?rhs")
proof -
have "?lhs = integralâ§N (distr μ (qbs_to_measure X) α) f"
by(simp add: nn_integral_distr)
also have "... = integralâ§N (distr ν (qbs_to_measure X) β) f"
by(simp add: qbs_prob_eq_dest(4)[OF h])
also have "... = ?rhs"
by(simp add: nn_integral_distr)
finally show ?thesis .
qed
qed simp
qed
lemma qbs_prob_eq_4_implies_3 :
assumes "qbs_prob_eq4 p1 p2"
shows "qbs_prob_eq3 p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq4_def)
note [simp] = qbs_prob_eq4_dest(3)[OF h]
show "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq3_intro)
fix f :: "'a â real"
assume [measurable]:"f â borel_measurable (qbs_to_measure X)"
and h': "âkâqbs_space X. 0 ⤠f k"
show "(â« x. f (α x) âμ) = (â« x. f (β x) âν)"
(is "?lhs = ?rhs")
proof -
have "?lhs = enn2real (â«â§+ x. ennreal (f (α x)) âμ)"
using h' by(auto simp: integral_eq_nn_integral[where f="(λx. f (α x))"] qbs_Mx_to_X(2))
also have "... = enn2real (â«â§+ x. (ennreal â f) (α x) âμ)"
by simp
also have "... = enn2real (â«â§+ x. (ennreal â f) (β x) âν)"
using qbs_prob_eq4_dest(4)[OF h,of "ennreal â f"] by simp
also have "... = enn2real (â«â§+ x. ennreal (f (β x)) âν)"
by simp
also have "... = ?rhs"
using h' by(auto simp: integral_eq_nn_integral[where f="(λx. f (β x))"] qbs_Mx_to_X(2))
finally show ?thesis .
qed
qed simp
qed
lemma qbs_prob_eq_equiv12 :
"qbs_prob_eq = qbs_prob_eq2"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_eq_equiv13 :
"qbs_prob_eq = qbs_prob_eq3"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_eq_equiv14 :
"qbs_prob_eq = qbs_prob_eq4"
using qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_4_implies_3 qbs_prob_eq_1_implies_2
by blast
lemma qbs_prob_eq_equiv23 :
"qbs_prob_eq2 = qbs_prob_eq3"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_eq_equiv24 :
"qbs_prob_eq2 = qbs_prob_eq4"
using qbs_prob_eq_2_implies_3 qbs_prob_eq_4_implies_3 qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_1_implies_2
by blast
lemma qbs_prob_eq_equiv34:
"qbs_prob_eq3 = qbs_prob_eq4"
using qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_4_implies_3
by blast
lemma qbs_prob_eq_equiv31 :
"qbs_prob_eq = qbs_prob_eq3"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_space_eq:
assumes "qbs_prob_eq (X,α,μ) (Y,β,ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using Quotient3_rel[OF Quotient3_qbs_prob_space] assms
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq:
assumes "Y = X"
and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using assms qbs_prob_eq_intro qbs_prob_space_eq by auto
lemma(in pair_qbs_prob) qbs_prob_space_eq2:
assumes "Y = X"
and "âf. f â qbs_to_measure X ââ©M real_borel
â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using qbs_prob_space_eq assms qbs_prob_eq_2_implies_3[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq_3_implies_1[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq2_intro qbs_prob_eq_dest(4)
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq3:
assumes "Y = X"
and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (âkâ qbs_space X. 0 ⤠f k)
â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using assms qbs_prob_eq_3_implies_1[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq3_intro qbs_prob_space_eq qbs_prob_eq_dest(4)
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq4:
assumes "Y = X"
and "âf. f â qbs_to_measure X ââ©M ennreal_borel
â¹ (â«â§+x. f (α x) â μ) = (â«â§+x. f (β x) â ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using assms qbs_prob_eq_4_implies_3[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_space_eq3[OF assms(1)] qbs_prob_eq3_dest(4) qbs_prob_eq4_intro
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq_inverse:
assumes "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
shows "qbs_prob_eq (X,α,μ) (Y,β,ν)"
and "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
and "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
and "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
using Quotient3_rel[OF Quotient3_qbs_prob_space,of "(X, α, μ)" "(Y,β,ν)",simplified] assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(simp_all add: qbs_prob_eq_equiv13[symmetric] qbs_prob_eq_equiv12[symmetric] qbs_prob_eq_equiv14[symmetric])
lift_definition qbs_prob_space_qbs :: "'a qbs_prob_space â 'a quasi_borel"
is fst by(auto simp add: qbs_prob_eq_def)
lemma(in qbs_prob) qbs_prob_space_qbs_computation[simp]:
"qbs_prob_space_qbs (qbs_prob_space (X,α,μ)) = X"
by(simp add: qbs_prob_space_qbs.abs_eq)
lemma rep_qbs_prob_space':
assumes "qbs_prob_space_qbs s = X"
shows "âα μ. s = qbs_prob_space (X,α,μ) â§ qbs_prob X α μ"
proof -
obtain X' α μ where hs:
"s = qbs_prob_space (X', α, μ)" "qbs_prob X' α μ"
using rep_qbs_prob_space[of s] by auto
then interpret qp:qbs_prob X' α μ
by simp
show ?thesis
using assms hs(2) by(auto simp add: hs(1))
qed
lift_definition qbs_prob_ennintegral :: "['a qbs_prob_space, 'a â ennreal] â ennreal"
is qbs_prob_t_ennintegral
by(auto simp add: qbs_prob_t_ennintegral_def qbs_prob_eq_equiv14 qbs_prob_eq4_def)
lift_definition qbs_prob_integral :: "['a qbs_prob_space, 'a â real] â real"
is qbs_prob_t_integral
by(auto simp add: qbs_prob_eq_equiv12 qbs_prob_t_integral_def qbs_prob_eq2_def)
syntax
"_qbs_prob_ennintegral" :: "pttrn â ennreal â 'a qbs_prob_space â ennreal" ("â«â§+â©Q((2 _./ _)/ â_)" [60,61] 110)
translations
"â«â§+â©Q x. f âp" â "CONST qbs_prob_ennintegral p (λx. f)"
syntax
"_qbs_prob_integral" :: "pttrn â real â 'a qbs_prob_space â real" ("â«â©Q((2 _./ _)/ â_)" [60,61] 110)
translations
"â«â©Q x. f âp" â "CONST qbs_prob_integral p (λx. f)"
text â¹ We define the function â¹lâ©X â L(P(X)) ââ©M G(X)âº. âº
lift_definition qbs_prob_measure :: "'a qbs_prob_space â 'a measure"
is qbs_prob_t_measure
by(auto simp add: qbs_prob_eq_def qbs_prob_t_measure_def)
declare [[coercion qbs_prob_measure]]
lemma(in qbs_prob) qbs_prob_measure_computation[simp]:
"qbs_prob_measure (qbs_prob_space (X,α,μ)) = distr μ (qbs_to_measure X) α"
by (simp add: qbs_prob_measure.abs_eq qbs_prob_t_measure_def)
definition qbs_emeasure ::"'a qbs_prob_space â 'a set â ennreal" where
"qbs_emeasure s â¡ emeasure (qbs_prob_measure s)"
lemma(in qbs_prob) qbs_emeasure_computation[simp]:
assumes "U â sets (qbs_to_measure X)"
shows "qbs_emeasure (qbs_prob_space (X,α,μ)) U = emeasure μ (α -` U)"
by(simp add: qbs_emeasure_def emeasure_distr[OF _ assms])
definition qbs_measure ::"'a qbs_prob_space â 'a set â real" where
"qbs_measure s â¡ measure (qbs_prob_measure s)"